Theorem sectepi

Description: If F is a section of G , then G is an epimorphism. 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 ) )