Theorem prstchomval

Description: Hom-sets of the constructed category which depend on an arbitrary definition. (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 )
	prstchomval.l	|- ( ph -> .<_ = ( le ` C ) )
Assertion	prstchomval	|- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		prstchomval.l	|- ( ph -> .<_ = ( le ` C ) )
4		homid	|- Hom = Slot ( Hom ` ndx )
5		slotsbhcdif	|- ( ( Base ` ndx ) =/= ( Hom ` ndx ) /\ ( Base ` ndx ) =/= ( comp ` ndx ) /\ ( Hom ` ndx ) =/= ( comp ` ndx ) )
6	5	simp3i	|- ( Hom ` ndx ) =/= ( comp ` ndx )
7	1 2 4 6	prstcnidlem	|- ( ph -> ( Hom ` C ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
8		fvex	|- ( le ` K ) e. _V
9		snex	|- { 1o } e. _V
10	8 9	xpex	|- ( ( le ` K ) X. { 1o } ) e. _V
11	4	setsid	|- ( ( K e. Proset /\ ( ( le ` K ) X. { 1o } ) e. _V ) -> ( ( le ` K ) X. { 1o } ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
12	2 10 11	sylancl	|- ( ph -> ( ( le ` K ) X. { 1o } ) = ( Hom ` ( K sSet <. ( Hom ` ndx ) , ( ( le ` K ) X. { 1o } ) >. ) ) )
13		eqidd	|- ( ph -> ( le ` K ) = ( le ` K ) )
14	1 2 13	prstcleval	|- ( ph -> ( le ` K ) = ( le ` C ) )
15	14 3	eqtr4d	|- ( ph -> ( le ` K ) = .<_ )
16	15	xpeq1d	|- ( ph -> ( ( le ` K ) X. { 1o } ) = ( .<_ X. { 1o } ) )
17	7 12 16	3eqtr2rd	|- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )