This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 ≤ 𝑌 ↔ ∃! 𝑓 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )