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

Metamath Proof Explorer

Theorem prstchom2ALT

Proof