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