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

Metamath Proof Explorer

Theorem thincmo2

Description: Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem1.1 ⊢ φ → X ∈ B
isthincd2lem1.2 ⊢ φ → Y ∈ B
isthincd2lem1.3 ⊢ φ → F ∈ X H Y
isthincd2lem1.4 ⊢ φ → G ∈ X H Y
thincmo2.b ⊢ B = Base C
thincmo2.h ⊢ H = Hom ⁡ C
thincmo2.c ⊢ φ → C ∈ ThinCat
Assertion thincmo2 ⊢ φ → F = G

Proof

Step Hyp Ref Expression
1 isthincd2lem1.1 ⊢ φ → X ∈ B
2 isthincd2lem1.2 ⊢ φ → Y ∈ B
3 isthincd2lem1.3 ⊢ φ → F ∈ X H Y
4 isthincd2lem1.4 ⊢ φ → G ∈ X H Y
5 thincmo2.b ⊢ B = Base C
6 thincmo2.h ⊢ H = Hom ⁡ C
7 thincmo2.c ⊢ φ → C ∈ ThinCat
8 5 6 isthinc ⊢ C ∈ ThinCat ↔ C ∈ Cat ∧ ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
9 8 simprbi ⊢ C ∈ ThinCat → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
10 7 9 syl ⊢ φ → ∀ x ∈ B ∀ y ∈ B ∃* f f ∈ x H y
11 1 2 3 4 10 isthincd2lem1 ⊢ φ → F = G