Theorem prstcnid

Description: Components other than Hom and comp are unchanged. (Contributed by Zhi Wang, 20-Sep-2024)

	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 )
	prstcnid.nh	|- ( E ` ndx ) =/= ( Hom ` ndx )
Assertion	prstcnid	|- ( ph -> ( E ` K ) = ( E ` C ) )

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		prstcnid.nh	|- ( E ` ndx ) =/= ( Hom ` ndx )
6	3 5	setsnid	|- ( E ` K ) = ( E ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) )
7	1 2 3 4	prstcnidlem	|- ( ph -> ( E ` C ) = ( E ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
8	6 7	eqtr4id	|- ( ph -> ( E ` K ) = ( E ` C ) )