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 } ) >. ) ) )