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 
|- ( ph -> C e. Cat )
idmon.x 
|- ( ph -> X e. B )
idmon.m 
|- M = ( Mono ` C )
Assertion idmon 
|- ( ph -> ( .1. ` X ) e. ( 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 
 |-  ( ph -> C e. Cat )
5 idmon.x 
 |-  ( ph -> X e. B )
6 idmon.m 
 |-  M = ( Mono ` C )
7 1 2 3 4 5 catidcl 
 |-  ( ph -> ( .1. ` X ) e. ( X H X ) )
8 4 adantr 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> C e. Cat )
9 simpr1 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> z e. B )
10 eqid 
 |-  ( comp ` C ) = ( comp ` C )
11 5 adantr 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> X e. B )
12 simpr2 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> g e. ( z H X ) )
13 1 2 3 8 9 10 11 12 catlid 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) g ) = g )
14 simpr3 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> h e. ( z H X ) )
15 1 2 3 8 9 10 11 14 catlid 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) h ) = h )
16 13 15 eqeq12d 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) g ) = ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) h ) <-> g = h ) )
17 16 biimpd 
 |-  ( ( ph /\ ( z e. B /\ g e. ( z H X ) /\ h e. ( z H X ) ) ) -> ( ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) g ) = ( ( .1. ` X ) ( <. z , X >. ( comp ` C ) X ) h ) -> g = h ) )
18 17 ralrimivvva 
 |-  ( ph -> A. z e. B A. g e. ( z H X ) A. h e. ( 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 
 |-  ( ph -> ( ( .1. ` X ) e. ( X M X ) <-> ( ( .1. ` X ) e. ( X H X ) /\ A. z e. B A. g e. ( z H X ) A. h e. ( 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 
 |-  ( ph -> ( .1. ` X ) e. ( X M X ) )