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=BaseC
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∈XEX

Proof

Step Hyp Ref Expression
1 idmon.b ⊢B=BaseC
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∈XHX
8 4 adantr ⊢φ∧z∈B∧g∈XHz∧h∈XHz→C∈Cat
9 5 adantr ⊢φ∧z∈B∧g∈XHz∧h∈XHz→X∈B
10 eqid ⊢comp⁡C=comp⁡C
11 simpr1 ⊢φ∧z∈B∧g∈XHz∧h∈XHz→z∈B
12 simpr2 ⊢φ∧z∈B∧g∈XHz∧h∈XHz→g∈XHz
13 1 2 3 8 9 10 11 12 catrid ⊢φ∧z∈B∧g∈XHz∧h∈XHz→gXXcomp⁡Cz1˙⁡X=g
14 simpr3 ⊢φ∧z∈B∧g∈XHz∧h∈XHz→h∈XHz
15 1 2 3 8 9 10 11 14 catrid ⊢φ∧z∈B∧g∈XHz∧h∈XHz→hXXcomp⁡Cz1˙⁡X=h
16 13 15 eqeq12d ⊢φ∧z∈B∧g∈XHz∧h∈XHz→gXXcomp⁡Cz1˙⁡X=hXXcomp⁡Cz1˙⁡X↔g=h
17 16 biimpd ⊢φ∧z∈B∧g∈XHz∧h∈XHz→gXXcomp⁡Cz1˙⁡X=hXXcomp⁡Cz1˙⁡X→g=h
18 17 ralrimivvva ⊢φ→∀z∈B∀g∈XHz∀h∈XHzgXXcomp⁡Cz1˙⁡X=hXXcomp⁡Cz1˙⁡X→g=h
19 1 2 10 6 4 5 5 isepi2 ⊢φ→1˙⁡X∈XEX↔1˙⁡X∈XHX∧∀z∈B∀g∈XHz∀h∈XHzgXXcomp⁡Cz1˙⁡X=hXXcomp⁡Cz1˙⁡X→g=h
20 7 18 19 mpbir2and ⊢φ→1˙⁡X∈XEX