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	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
	prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
	prstchom.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
	prstchom.e	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
Assertion	prstchom2ALT	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		prstcnid.c	⊢ ( 𝜑 → 𝐶 = ( ProsetToCat ‘ 𝐾 ) )
2		prstcnid.k	⊢ ( 𝜑 → 𝐾 ∈ Proset )
3		prstchom.l	⊢ ( 𝜑 → ≤ = ( le ‘ 𝐶 ) )
4		prstchom.e	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
5		ovex	⊢ ( 𝑋 𝐻 𝑌 ) ∈ V
6	1 2 3	prstchomval	⊢ ( 𝜑 → ( ≤ × { 1o } ) = ( Hom ‘ 𝐶 ) )
7	4 6	eqtr4d	⊢ ( 𝜑 → 𝐻 = ( ≤ × { 1o } ) )
8		1oex	⊢ 1o ∈ V
9	8	a1i	⊢ ( 𝜑 → 1o ∈ V )
10		1n0	⊢ 1o ≠ ∅
11	10	a1i	⊢ ( 𝜑 → 1o ≠ ∅ )
12	7 9 11	fvconstr	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) = 1o ) )
13	12	biimpa	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 𝐻 𝑌 ) = 1o )
14		eqeng	⊢ ( ( 𝑋 𝐻 𝑌 ) ∈ V → ( ( 𝑋 𝐻 𝑌 ) = 1o → ( 𝑋 𝐻 𝑌 ) ≈ 1o ) )
15	5 13 14	mpsyl	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ( 𝑋 𝐻 𝑌 ) ≈ 1o )
16		euen1b	⊢ ( ( 𝑋 𝐻 𝑌 ) ≈ 1o ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
17	15 16	sylib	⊢ ( ( 𝜑 ∧ 𝑋 ≤ 𝑌 ) → ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
18		euex	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
19		n0	⊢ ( ( 𝑋 𝐻 𝑌 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) )
20	18 19	sylibr	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) → ( 𝑋 𝐻 𝑌 ) ≠ ∅ )
21	7 9 11	fvconstrn0	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) )
22	21	biimpar	⊢ ( ( 𝜑 ∧ ( 𝑋 𝐻 𝑌 ) ≠ ∅ ) → 𝑋 ≤ 𝑌 )
23	20 22	sylan2	⊢ ( ( 𝜑 ∧ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) → 𝑋 ≤ 𝑌 )
24	17 23	impbida	⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )