Metamath Proof Explorer

Theorem monsect

Description: If F is a monomorphism and G is a section of F , then G is an inverse of F and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (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 )
monsect.n 
|- N = ( Inv ` C )
monsect.1 
|- ( ph -> F e. ( X M Y ) )
monsect.2 
|- ( ph -> G ( Y S X ) F )
Assertion monsect 
|- ( ph -> F ( X N Y ) G )

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 monsect.n 
 |-  N = ( Inv ` C )
8 monsect.1 
 |-  ( ph -> F e. ( X M Y ) )
9 monsect.2 
 |-  ( ph -> G ( Y S X ) F )
10 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
11 eqid 
 |-  ( comp ` C ) = ( comp ` C )
12 eqid 
 |-  ( Id ` C ) = ( Id ` C )
13 1 10 11 12 3 4 6 5 issect 
 |-  ( ph -> ( G ( Y S X ) F <-> ( G e. ( Y ( Hom ` C ) X ) /\ F e. ( X ( Hom ` C ) Y ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) G ) = ( ( Id ` C ) ` Y ) ) ) )
14 9 13 mpbid 
 |-  ( ph -> ( G e. ( Y ( Hom ` C ) X ) /\ F e. ( X ( Hom ` C ) Y ) /\ ( F ( <. Y , X >. ( comp ` C ) Y ) G ) = ( ( Id ` C ) ` Y ) ) )
15 14 simp3d 
 |-  ( ph -> ( F ( <. Y , X >. ( comp ` C ) Y ) G ) = ( ( Id ` C ) ` Y ) )
16 15 oveq1d 
 |-  ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) G ) ( <. X , Y >. ( comp ` C ) Y ) F ) = ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) )
17 14 simp2d 
 |-  ( ph -> F e. ( X ( Hom ` C ) Y ) )
18 14 simp1d 
 |-  ( ph -> G e. ( Y ( Hom ` C ) X ) )
19 1 10 11 4 5 6 5 17 18 6 17 catass 
 |-  ( ph -> ( ( F ( <. Y , X >. ( comp ` C ) Y ) G ) ( <. X , Y >. ( comp ` C ) Y ) F ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( G ( <. X , Y >. ( comp ` C ) X ) F ) ) )
20 1 10 12 4 5 11 6 17 catlid 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) = F )
21 1 10 12 4 5 11 6 17 catrid 
 |-  ( ph -> ( F ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) = F )
22 20 21 eqtr4d 
 |-  ( ph -> ( ( ( Id ` C ) ` Y ) ( <. X , Y >. ( comp ` C ) Y ) F ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) )
23 16 19 22 3eqtr3d 
 |-  ( ph -> ( F ( <. X , X >. ( comp ` C ) Y ) ( G ( <. X , Y >. ( comp ` C ) X ) F ) ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) )
24 1 10 11 4 5 6 5 17 18 catcocl 
 |-  ( ph -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) e. ( X ( Hom ` C ) X ) )
25 1 10 12 4 5 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
26 1 10 11 2 4 5 6 5 8 24 25 moni 
 |-  ( ph -> ( ( F ( <. X , X >. ( comp ` C ) Y ) ( G ( <. X , Y >. ( comp ` C ) X ) F ) ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( ( Id ` C ) ` X ) ) <-> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
27 23 26 mpbid 
 |-  ( ph -> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) )
28 1 10 11 12 3 4 5 6 17 18 issect2 
 |-  ( ph -> ( F ( X S Y ) G <-> ( G ( <. X , Y >. ( comp ` C ) X ) F ) = ( ( Id ` C ) ` X ) ) )
29 27 28 mpbird 
 |-  ( ph -> F ( X S Y ) G )
30 1 7 4 5 6 3 isinv 
 |-  ( ph -> ( F ( X N Y ) G <-> ( F ( X S Y ) G /\ G ( Y S X ) F ) ) )
31 29 9 30 mpbir2and 
 |-  ( ph -> F ( X N Y ) G )