Metamath Proof Explorer

Theorem thincmon

Description: In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon . (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincid.c ⊢ φ → C ∈ ThinCat
thincid.b ⊢ B = Base C
thincid.h ⊢ H = Hom ⁡ C
thincid.x ⊢ φ → X ∈ B
thincmon.y ⊢ φ → Y ∈ B
thincmon.m ⊢ M = Mono ⁡ C
Assertion thincmon ⊢ φ → X M Y = X H Y

Proof

Step Hyp Ref Expression
1 thincid.c ⊢ φ → C ∈ ThinCat
2 thincid.b ⊢ B = Base C
3 thincid.h ⊢ H = Hom ⁡ C
4 thincid.x ⊢ φ → X ∈ B
5 thincmon.y ⊢ φ → Y ∈ B
6 thincmon.m ⊢ M = Mono ⁡ C
7 simpr1 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → z ∈ B
8 4 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → X ∈ B
9 simpr2 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → g ∈ z H X
10 simpr3 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → h ∈ z H X
11 1 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → C ∈ ThinCat
12 7 8 9 10 2 3 11 thincmo2 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → g = h
13 12 a1d ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → f z X comp ⁡ C Y g = f z X comp ⁡ C Y h → g = h
14 13 ralrimivvva ⊢ φ → ∀ z ∈ B ∀ g ∈ z H X ∀ h ∈ z H X f z X comp ⁡ C Y g = f z X comp ⁡ C Y h → g = h
15 eqid ⊢ comp ⁡ C = comp ⁡ C
16 1 thinccd ⊢ φ → C ∈ Cat
17 2 3 15 6 16 4 5 ismon2 ⊢ φ → f ∈ X M Y ↔ f ∈ X H Y ∧ ∀ z ∈ B ∀ g ∈ z H X ∀ h ∈ z H X f z X comp ⁡ C Y g = f z X comp ⁡ C Y h → g = h
18 14 17 mpbiran2d ⊢ φ → f ∈ X M Y ↔ f ∈ X H Y
19 18 eqrdv ⊢ φ → X M Y = X H Y