Metamath Proof Explorer

Theorem idmon

Description: An identity arrow, or an identity morphism, is a monomorphism. (Contributed by Zhi Wang, 21-Sep-2024)

Ref Expression
Hypotheses idmon.b ⊢ B = Base C
idmon.h ⊢ H = Hom ⁡ C
idmon.i ⊢ 1 ˙ = Id ⁡ C
idmon.c ⊢ φ → C ∈ Cat
idmon.x ⊢ φ → X ∈ B
idmon.m ⊢ M = Mono ⁡ C
Assertion idmon ⊢ φ → 1 ˙ ⁡ X ∈ X M X

Proof

Step Hyp Ref Expression
1 idmon.b ⊢ B = Base C
2 idmon.h ⊢ H = Hom ⁡ C
3 idmon.i ⊢ 1 ˙ = Id ⁡ C
4 idmon.c ⊢ φ → C ∈ Cat
5 idmon.x ⊢ φ → X ∈ B
6 idmon.m ⊢ M = Mono ⁡ C
7 1 2 3 4 5 catidcl ⊢ φ → 1 ˙ ⁡ X ∈ X H X
8 4 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → C ∈ Cat
9 simpr1 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → z ∈ B
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 5 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → X ∈ B
12 simpr2 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → g ∈ z H X
13 1 2 3 8 9 10 11 12 catlid ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → 1 ˙ ⁡ X z X comp ⁡ C X g = g
14 simpr3 ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → h ∈ z H X
15 1 2 3 8 9 10 11 14 catlid ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → 1 ˙ ⁡ X z X comp ⁡ C X h = h
16 13 15 eqeq12d ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → 1 ˙ ⁡ X z X comp ⁡ C X g = 1 ˙ ⁡ X z X comp ⁡ C X h ↔ g = h
17 16 biimpd ⊢ φ ∧ z ∈ B ∧ g ∈ z H X ∧ h ∈ z H X → 1 ˙ ⁡ X z X comp ⁡ C X g = 1 ˙ ⁡ X z X comp ⁡ C X h → g = h
18 17 ralrimivvva ⊢ φ → ∀ z ∈ B ∀ g ∈ z H X ∀ h ∈ z H X 1 ˙ ⁡ X z X comp ⁡ C X g = 1 ˙ ⁡ X z X comp ⁡ C X h → g = h
19 1 2 10 6 4 5 5 ismon2 ⊢ φ → 1 ˙ ⁡ X ∈ X M X ↔ 1 ˙ ⁡ X ∈ X H X ∧ ∀ z ∈ B ∀ g ∈ z H X ∀ h ∈ z H X 1 ˙ ⁡ X z X comp ⁡ C X g = 1 ˙ ⁡ X z X comp ⁡ C X h → g = h
20 7 18 19 mpbir2and ⊢ φ → 1 ˙ ⁡ X ∈ X M X