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

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 idmon.m ⊢M=Mono⁡C
7 1 2 3 4 5 catidcl ⊢φ→1˙⁡X∈XHX
8 4 adantr ⊢φ∧z∈B∧g∈zHX∧h∈zHX→C∈Cat
9 simpr1 ⊢φ∧z∈B∧g∈zHX∧h∈zHX→z∈B
10 eqid ⊢comp⁡C=comp⁡C
11 5 adantr ⊢φ∧z∈B∧g∈zHX∧h∈zHX→X∈B
12 simpr2 ⊢φ∧z∈B∧g∈zHX∧h∈zHX→g∈zHX
13 1 2 3 8 9 10 11 12 catlid ⊢φ∧z∈B∧g∈zHX∧h∈zHX→1˙⁡XzXcomp⁡CXg=g
14 simpr3 ⊢φ∧z∈B∧g∈zHX∧h∈zHX→h∈zHX
15 1 2 3 8 9 10 11 14 catlid ⊢φ∧z∈B∧g∈zHX∧h∈zHX→1˙⁡XzXcomp⁡CXh=h
16 13 15 eqeq12d ⊢φ∧z∈B∧g∈zHX∧h∈zHX→1˙⁡XzXcomp⁡CXg=1˙⁡XzXcomp⁡CXh↔g=h
17 16 biimpd ⊢φ∧z∈B∧g∈zHX∧h∈zHX→1˙⁡XzXcomp⁡CXg=1˙⁡XzXcomp⁡CXh→g=h
18 17 ralrimivvva ⊢φ→∀z∈B∀g∈zHX∀h∈zHX1˙⁡XzXcomp⁡CXg=1˙⁡XzXcomp⁡CXh→g=h
19 1 2 10 6 4 5 5 ismon2 ⊢φ→1˙⁡X∈XMX↔1˙⁡X∈XHX∧∀z∈B∀g∈zHX∀h∈zHX1˙⁡XzXcomp⁡CXg=1˙⁡XzXcomp⁡CXh→g=h
20 7 18 19 mpbir2and ⊢φ→1˙⁡X∈XMX