Metamath Proof Explorer

Theorem idepi

Description: An identity arrow, or an identity morphism, is an epimorphism. (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
idepi.e ⊢ E = Epi ⁡ C
Assertion idepi ⊢ φ → 1 ˙ ⁡ X ∈ X E 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 idepi.e ⊢ E = Epi ⁡ C
7 1 2 3 4 5 catidcl ⊢ φ → 1 ˙ ⁡ X ∈ X H X
8 4 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → C ∈ Cat
9 5 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → X ∈ B
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 simpr1 ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → z ∈ B
12 simpr2 ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → g ∈ X H z
13 1 2 3 8 9 10 11 12 catrid ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → g X X comp ⁡ C z 1 ˙ ⁡ X = g
14 simpr3 ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → h ∈ X H z
15 1 2 3 8 9 10 11 14 catrid ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → h X X comp ⁡ C z 1 ˙ ⁡ X = h
16 13 15 eqeq12d ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → g X X comp ⁡ C z 1 ˙ ⁡ X = h X X comp ⁡ C z 1 ˙ ⁡ X ↔ g = h
17 16 biimpd ⊢ φ ∧ z ∈ B ∧ g ∈ X H z ∧ h ∈ X H z → g X X comp ⁡ C z 1 ˙ ⁡ X = h X X comp ⁡ C z 1 ˙ ⁡ X → g = h
18 17 ralrimivvva ⊢ φ → ∀ z ∈ B ∀ g ∈ X H z ∀ h ∈ X H z g X X comp ⁡ C z 1 ˙ ⁡ X = h X X comp ⁡ C z 1 ˙ ⁡ X → g = h
19 1 2 10 6 4 5 5 isepi2 ⊢ φ → 1 ˙ ⁡ X ∈ X E X ↔ 1 ˙ ⁡ X ∈ X H X ∧ ∀ z ∈ B ∀ g ∈ X H z ∀ h ∈ X H z g X X comp ⁡ C z 1 ˙ ⁡ X = h X X comp ⁡ C z 1 ˙ ⁡ X → g = h
20 7 18 19 mpbir2and ⊢ φ → 1 ˙ ⁡ X ∈ X E X