Theorem prstchom2ALT

Description: Hom-sets of the constructed category are dependent on the preorder. This proof depends on the definition df-prstc . See prstchom2 for a version that does not depend on the definition. (Contributed by Zhi Wang, 20-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
	prstcnid.k	|- ( ph -> K e. Proset )
	prstchom.l	|- ( ph -> .<_ = ( le ` C ) )
	prstchom.e	|- ( ph -> H = ( Hom ` C ) )
Assertion	prstchom2ALT	|- ( ph -> ( X .<_ Y <-> E! f f e. ( X H Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	|- ( ph -> C = ( ProsetToCat ` K ) )
2		prstcnid.k	|- ( ph -> K e. Proset )
3		prstchom.l	|- ( ph -> .<_ = ( le ` C ) )
4		prstchom.e	|- ( ph -> H = ( Hom ` C ) )
5		ovex	|- ( X H Y ) e. _V
6	1 2 3	prstchomval	|- ( ph -> ( .<_ X. { 1o } ) = ( Hom ` C ) )
7	4 6	eqtr4d	|- ( ph -> H = ( .<_ X. { 1o } ) )
8		1oex	|- 1o e. _V
9	8	a1i	|- ( ph -> 1o e. _V )
10		1n0	|- 1o =/= (/)
11	10	a1i	|- ( ph -> 1o =/= (/) )
12	7 9 11	fvconstr	|- ( ph -> ( X .<_ Y <-> ( X H Y ) = 1o ) )
13	12	biimpa	|- ( ( ph /\ X .<_ Y ) -> ( X H Y ) = 1o )
14		eqeng	|- ( ( X H Y ) e. _V -> ( ( X H Y ) = 1o -> ( X H Y ) ~~ 1o ) )
15	5 13 14	mpsyl	|- ( ( ph /\ X .<_ Y ) -> ( X H Y ) ~~ 1o )
16		euen1b	|- ( ( X H Y ) ~~ 1o <-> E! f f e. ( X H Y ) )
17	15 16	sylib	|- ( ( ph /\ X .<_ Y ) -> E! f f e. ( X H Y ) )
18		euex	|- ( E! f f e. ( X H Y ) -> E. f f e. ( X H Y ) )
19		n0	|- ( ( X H Y ) =/= (/) <-> E. f f e. ( X H Y ) )
20	18 19	sylibr	|- ( E! f f e. ( X H Y ) -> ( X H Y ) =/= (/) )
21	7 9 11	fvconstrn0	|- ( ph -> ( X .<_ Y <-> ( X H Y ) =/= (/) ) )
22	21	biimpar	|- ( ( ph /\ ( X H Y ) =/= (/) ) -> X .<_ Y )
23	20 22	sylan2	|- ( ( ph /\ E! f f e. ( X H Y ) ) -> X .<_ Y )
24	17 23	impbida	|- ( ph -> ( X .<_ Y <-> E! f f e. ( X H Y ) ) )