Metamath Proof Explorer

Theorem episect

Description: If F is an epimorphism and F is a section of G , then G is an inverse of F and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses sectepi.b 
|- B = ( Base ` C )
sectepi.e 
|- E = ( Epi ` C )
sectepi.s 
|- S = ( Sect ` C )
sectepi.c 
|- ( ph -> C e. Cat )
sectepi.x 
|- ( ph -> X e. B )
sectepi.y 
|- ( ph -> Y e. B )
episect.n 
|- N = ( Inv ` C )
episect.1 
|- ( ph -> F e. ( X E Y ) )
episect.2 
|- ( ph -> F ( X S Y ) G )
Assertion episect 
|- ( ph -> F ( X N Y ) G )

Proof

Step Hyp Ref Expression
1 sectepi.b 
 |-  B = ( Base ` C )
2 sectepi.e 
 |-  E = ( Epi ` C )
3 sectepi.s 
 |-  S = ( Sect ` C )
4 sectepi.c 
 |-  ( ph -> C e. Cat )
5 sectepi.x 
 |-  ( ph -> X e. B )
6 sectepi.y 
 |-  ( ph -> Y e. B )
7 episect.n 
 |-  N = ( Inv ` C )
8 episect.1 
 |-  ( ph -> F e. ( X E Y ) )
9 episect.2 
 |-  ( ph -> F ( X S Y ) G )
10 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
11 eqid 
 |-  ( Inv ` ( oppCat ` C ) ) = ( Inv ` ( oppCat ` C ) )
12 1 10 4 6 5 7 11 oppcinv 
 |-  ( ph -> ( Y ( Inv ` ( oppCat ` C ) ) X ) = ( X N Y ) )
13 10 1 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
14 eqid 
 |-  ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) )
15 eqid 
 |-  ( Sect ` ( oppCat ` C ) ) = ( Sect ` ( oppCat ` C ) )
16 10 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
17 4 16 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
18 10 4 14 2 oppcmon 
 |-  ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) )
19 8 18 eleqtrrd 
 |-  ( ph -> F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) )
20 1 10 4 5 6 3 15 oppcsect 
 |-  ( ph -> ( G ( X ( Sect ` ( oppCat ` C ) ) Y ) F <-> F ( X S Y ) G ) )
21 9 20 mpbird 
 |-  ( ph -> G ( X ( Sect ` ( oppCat ` C ) ) Y ) F )
22 13 14 15 17 6 5 11 19 21 monsect 
 |-  ( ph -> F ( Y ( Inv ` ( oppCat ` C ) ) X ) G )
23 12 22 breqdi 
 |-  ( ph -> F ( X N Y ) G )