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

Metamath Proof Explorer

Theorem thincmod

Description: At most one morphism in each hom-set (deduction form). (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses thincmo.c ⊢ φ → C ∈ ThinCat
thincmo.x ⊢ φ → X ∈ B
thincmo.y ⊢ φ → Y ∈ B
thincn0eu.b ⊢ φ → B = Base C
thincn0eu.h ⊢ φ → H = Hom ⁡ C
Assertion thincmod ⊢ φ → ∃* 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 thincn0eu.b ⊢ φ → B = Base C
5 thincn0eu.h ⊢ φ → H = Hom ⁡ C
6 2 4 eleqtrd ⊢ φ → X ∈ Base C
7 3 4 eleqtrd ⊢ φ → Y ∈ Base C
8 eqid ⊢ Base C = Base C
9 eqid ⊢ Hom ⁡ C = Hom ⁡ C
10 1 6 7 8 9 thincmo ⊢ φ → ∃* f f ∈ X Hom ⁡ C Y
11 5 oveqd ⊢ φ → X H Y = X Hom ⁡ C Y
12 11 eleq2d ⊢ φ → f ∈ X H Y ↔ f ∈ X Hom ⁡ C Y
13 12 mobidv ⊢ φ → ∃* f f ∈ X H Y ↔ ∃* f f ∈ X Hom ⁡ C Y
14 10 13 mpbird ⊢ φ → ∃* f f ∈ X H Y