Metamath Proof Explorer

Theorem thincmo

Description: There is at most one morphism in each hom-set. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses thincmo.c ⊢ φ → C ∈ ThinCat
thincmo.x ⊢ φ → X ∈ B
thincmo.y ⊢ φ → Y ∈ B
thincmo.b ⊢ B = Base C
thincmo.h ⊢ H = Hom ⁡ C
Assertion thincmo ⊢ φ → ∃* f f ∈ X H Y

Proof

Step Hyp Ref Expression
1 thincmo.c ⊢ φ → C ∈ ThinCat
2 thincmo.x ⊢ φ → X ∈ B
3 thincmo.y ⊢ φ → Y ∈ B
4 thincmo.b ⊢ B = Base C
5 thincmo.h ⊢ H = Hom ⁡ C
6 2 adantr ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → X ∈ B
7 3 adantr ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → Y ∈ B
8 simprl ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → f ∈ X H Y
9 simprr ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → g ∈ X H Y
10 1 adantr ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → C ∈ ThinCat
11 6 7 8 9 4 5 10 thincmo2 ⊢ φ ∧ f ∈ X H Y ∧ g ∈ X H Y → f = g
12 11 ex ⊢ φ → f ∈ X H Y ∧ g ∈ X H Y → f = g
13 12 alrimivv ⊢ φ → ∀ f ∀ g f ∈ X H Y ∧ g ∈ X H Y → f = g
14 eleq1w ⊢ f = g → f ∈ X H Y ↔ g ∈ X H Y
15 14 mo4 ⊢ ∃* f f ∈ X H Y ↔ ∀ f ∀ g f ∈ X H Y ∧ g ∈ X H Y → f = g
16 13 15 sylibr ⊢ φ → ∃* f f ∈ X H Y