This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prstcnidlem

Description: Lemma for prstcnid and prstchomval . (Contributed by Zhi Wang, 20-Sep-2024) (New usage is discouraged.)

Ref Expression
Hypotheses prstcnid.c 
|- ( ph -> C = ( ProsetToCat ` K ) )
prstcnid.k 
|- ( ph -> K e. Proset )
prstcnid.e 
|- E = Slot ( E ` ndx )
prstcnid.no 
|- ( E ` ndx ) =/= ( comp ` ndx )
Assertion prstcnidlem 
|- ( ph -> ( E ` C ) = ( E ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )

Proof

Step Hyp Ref Expression
1 prstcnid.c 
 |-  ( ph -> C = ( ProsetToCat ` K ) )
2 prstcnid.k 
 |-  ( ph -> K e. Proset )
3 prstcnid.e 
 |-  E = Slot ( E ` ndx )
4 prstcnid.no 
 |-  ( E ` ndx ) =/= ( comp ` ndx )
5 1 2 prstcval 
 |-  ( ph -> C = ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
6 5 fveq2d 
 |-  ( ph -> ( E ` C ) = ( E ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) ) )
7 3 4 setsnid 
 |-  ( E ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) = ( E ` ( ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) sSet <. ( comp ` ndx ) , (/) >. ) )
8 6 7 eqtr4di 
 |-  ( ph -> ( E ` C ) = ( E ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )