Metamath Proof Explorer

Theorem sectmon

Description: If F is a section of G , then F is a monomorphism. A monomorphism that arises from a section is also known as asplit monomorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses sectmon.b 
|- B = ( Base ` C )
sectmon.m 
|- M = ( Mono ` C )
sectmon.s 
|- S = ( Sect ` C )
sectmon.c 
|- ( ph -> C e. Cat )
sectmon.x 
|- ( ph -> X e. B )
sectmon.y 
|- ( ph -> Y e. B )
sectmon.1 
|- ( ph -> F ( X S Y ) G )
Assertion sectmon 
|- ( ph -> F e. ( X M Y ) )

Proof

Step Hyp Ref Expression
1 sectmon.b 
 |-  B = ( Base ` C )
2 sectmon.m 
 |-  M = ( Mono ` C )
3 sectmon.s 
 |-  S = ( Sect ` C )
4 sectmon.c 
 |-  ( ph -> C e. Cat )
5 sectmon.x 
 |-  ( ph -> X e. B )
6 sectmon.y 
 |-  ( ph -> Y e. B )
7 sectmon.1 
 |-  ( ph -> F ( X S Y ) G )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 eqid 
 |-  ( Id ` C ) = ( Id ` C )
11 1 8 9 10 3 4 5 6 issect 
 |-  ( ph -> ( F ( X S Y ) G <-> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) ) )
12 7 11 mpbid 
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) /\ G e. ( Y ( Hom ` C ) X ) /\ ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
13 12 simp1d 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
14 oveq2 
 |-  ( ( F ( <. x , X >. ( comp ` C ) Y ) g ) = ( F ( <. x , X >. ( comp ` C ) Y ) h ) -> ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) g ) ) = ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) h ) ) )
15 12 simp3d 
 |-  ( ph -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) )
16 15 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) )
17 16 oveq1d 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) ( <. x , X >. ( comp ` C ) X ) g ) = ( ( ( Id ` C ) ` X ) ( <. x , X >. ( comp ` C ) X ) g ) )
18 4 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> C e. Cat )
19 simplr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> x e. B )
20 5 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> X e. B )
21 6 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> Y e. B )
22 simprl 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> g e. ( x ( Hom ` C ) X ) )
23 13 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> F e. ( X ( Hom ` C ) Y ) )
24 12 simp2d 
 |-  ( ph -> G e. ( Y ( Hom ` C ) X ) )
25 24 ad2antrr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> G e. ( Y ( Hom ` C ) X ) )
26 1 8 9 18 19 20 21 22 23 20 25 catass 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) ( <. x , X >. ( comp ` C ) X ) g ) = ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) g ) ) )
27 1 8 10 18 19 9 20 22 catlid 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( ( Id ` C ) ` X ) ( <. x , X >. ( comp ` C ) X ) g ) = g )
28 17 26 27 3eqtr3d 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) g ) ) = g )
29 16 oveq1d 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) ( <. x , X >. ( comp ` C ) X ) h ) = ( ( ( Id ` C ) ` X ) ( <. x , X >. ( comp ` C ) X ) h ) )
30 simprr 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> h e. ( x ( Hom ` C ) X ) )
31 1 8 9 18 19 20 21 30 23 20 25 catass 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( G ( <. X , Y >. ( comp ` C ) X ) F ) ( <. x , X >. ( comp ` C ) X ) h ) = ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) h ) ) )
32 1 8 10 18 19 9 20 30 catlid 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( ( Id ` C ) ` X ) ( <. x , X >. ( comp ` C ) X ) h ) = h )
33 29 31 32 3eqtr3d 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) h ) ) = h )
34 28 33 eqeq12d 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) g ) ) = ( G ( <. x , Y >. ( comp ` C ) X ) ( F ( <. x , X >. ( comp ` C ) Y ) h ) ) <-> g = h ) )
35 14 34 syl5ib 
 |-  ( ( ( ph /\ x e. B ) /\ ( g e. ( x ( Hom ` C ) X ) /\ h e. ( x ( Hom ` C ) X ) ) ) -> ( ( F ( <. x , X >. ( comp ` C ) Y ) g ) = ( F ( <. x , X >. ( comp ` C ) Y ) h ) -> g = h ) )
36 35 ralrimivva 
 |-  ( ( ph /\ x e. B ) -> A. g e. ( x ( Hom ` C ) X ) A. h e. ( x ( Hom ` C ) X ) ( ( F ( <. x , X >. ( comp ` C ) Y ) g ) = ( F ( <. x , X >. ( comp ` C ) Y ) h ) -> g = h ) )
37 36 ralrimiva 
 |-  ( ph -> A. x e. B A. g e. ( x ( Hom ` C ) X ) A. h e. ( x ( Hom ` C ) X ) ( ( F ( <. x , X >. ( comp ` C ) Y ) g ) = ( F ( <. x , X >. ( comp ` C ) Y ) h ) -> g = h ) )
38 1 8 9 2 4 5 6 ismon2 
 |-  ( ph -> ( F e. ( X M Y ) <-> ( F e. ( X ( Hom ` C ) Y ) /\ A. x e. B A. g e. ( x ( Hom ` C ) X ) A. h e. ( x ( Hom ` C ) X ) ( ( F ( <. x , X >. ( comp ` C ) Y ) g ) = ( F ( <. x , X >. ( comp ` C ) Y ) h ) -> g = h ) ) ) )
39 13 37 38 mpbir2and 
 |-  ( ph -> F e. ( X M Y ) )