This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sectepi

Description: If F is a section of G , then G is an epimorphism. Proposition 7.42 of Adamek p. 112. An epimorphism that arises from a section is also known as asplit epimorphism. (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 )
sectepi.1 
|- ( ph -> F ( X S Y ) G )
Assertion sectepi 
|- ( ph -> G e. ( Y E X ) )

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 sectepi.1 
 |-  ( ph -> F ( X S Y ) G )
8 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
9 8 1 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
10 eqid 
 |-  ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) )
11 eqid 
 |-  ( Sect ` ( oppCat ` C ) ) = ( Sect ` ( oppCat ` C ) )
12 8 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
13 4 12 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
14 1 8 4 5 6 3 11 oppcsect 
 |-  ( ph -> ( G ( X ( Sect ` ( oppCat ` C ) ) Y ) F <-> F ( X S Y ) G ) )
15 7 14 mpbird 
 |-  ( ph -> G ( X ( Sect ` ( oppCat ` C ) ) Y ) F )
16 9 10 11 13 5 6 15 sectmon 
 |-  ( ph -> G e. ( X ( Mono ` ( oppCat ` C ) ) Y ) )
17 8 4 10 2 oppcmon 
 |-  ( ph -> ( X ( Mono ` ( oppCat ` C ) ) Y ) = ( Y E X ) )
18 16 17 eleqtrd 
 |-  ( ph -> G e. ( Y E X ) )