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 ⊢ φ → C = ProsetToCat ⁡ K
prstcnid.k ⊢ φ → K ∈ Proset
prstchom.l ⊢ φ → ≤ ˙ = ≤ C
prstchom.e ⊢ φ → H = Hom ⁡ C
Assertion prstchom2ALT ⊢ φ → X ≤ ˙ Y ↔ ∃! f f ∈ X H Y

Proof

Step Hyp Ref Expression
1 prstcnid.c ⊢ φ → C = ProsetToCat ⁡ K
2 prstcnid.k ⊢ φ → K ∈ Proset
3 prstchom.l ⊢ φ → ≤ ˙ = ≤ C
4 prstchom.e ⊢ φ → H = Hom ⁡ C
5 ovex ⊢ X H Y ∈ V
6 1 2 3 prstchomval ⊢ φ → ≤ ˙ × 1 𝑜 = Hom ⁡ C
7 4 6 eqtr4d ⊢ φ → H = ≤ ˙ × 1 𝑜
8 1oex ⊢ 1 𝑜 ∈ V
9 8 a1i ⊢ φ → 1 𝑜 ∈ V
10 1n0 ⊢ 1 𝑜 ≠ ∅
11 10 a1i ⊢ φ → 1 𝑜 ≠ ∅
12 7 9 11 fvconstr ⊢ φ → X ≤ ˙ Y ↔ X H Y = 1 𝑜
13 12 biimpa ⊢ φ ∧ X ≤ ˙ Y → X H Y = 1 𝑜
14 eqeng ⊢ X H Y ∈ V → X H Y = 1 𝑜 → X H Y ≈ 1 𝑜
15 5 13 14 mpsyl ⊢ φ ∧ X ≤ ˙ Y → X H Y ≈ 1 𝑜
16 euen1b ⊢ X H Y ≈ 1 𝑜 ↔ ∃! f f ∈ X H Y
17 15 16 sylib ⊢ φ ∧ X ≤ ˙ Y → ∃! f f ∈ X H Y
18 euex ⊢ ∃! f f ∈ X H Y → ∃ f f ∈ X H Y
19 n0 ⊢ X H Y ≠ ∅ ↔ ∃ f f ∈ X H Y
20 18 19 sylibr ⊢ ∃! f f ∈ X H Y → X H Y ≠ ∅
21 7 9 11 fvconstrn0 ⊢ φ → X ≤ ˙ Y ↔ X H Y ≠ ∅
22 21 biimpar ⊢ φ ∧ X H Y ≠ ∅ → X ≤ ˙ Y
23 20 22 sylan2 ⊢ φ ∧ ∃! f f ∈ X H Y → X ≤ ˙ Y
24 17 23 impbida ⊢ φ → X ≤ ˙ Y ↔ ∃! f f ∈ X H Y