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={\mathrm{Base}}_C$$
	sectepi.e	$$⊢E=\mathrm{Epi}\left(C\right)$$
	sectepi.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
	sectepi.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	sectepi.x	$$⊢\phi \to X\in B$$
	sectepi.y	$$⊢\phi \to Y\in B$$
	sectepi.1	$$⊢\phi \to F\left(XSY\right)G$$
Assertion	sectepi	$$⊢\phi \to G\in \left(YEX\right)$$

Proof

Step	Hyp	Ref	Expression
1		sectepi.b	$$⊢B={\mathrm{Base}}_C$$
2		sectepi.e	$$⊢E=\mathrm{Epi}\left(C\right)$$
3		sectepi.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
4		sectepi.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		sectepi.x	$$⊢\phi \to X\in B$$
6		sectepi.y	$$⊢\phi \to Y\in B$$
7		sectepi.1	$$⊢\phi \to F\left(XSY\right)G$$
8		eqid	$$⊢\mathrm{oppCat}\left(C\right)=\mathrm{oppCat}\left(C\right)$$
9	8 1	oppcbas	$$⊢B={\mathrm{Base}}_{\mathrm{oppCat}\left(C\right)}$$
10		eqid	$$⊢\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)$$
11		eqid	$$⊢\mathrm{Sect}\left(\mathrm{oppCat}\left(C\right)\right)=\mathrm{Sect}\left(\mathrm{oppCat}\left(C\right)\right)$$
12	8	oppccat	$$⊢C\in \mathrm{Cat}\to \mathrm{oppCat}\left(C\right)\in \mathrm{Cat}$$
13	4 12	syl	$$⊢\phi \to \mathrm{oppCat}\left(C\right)\in \mathrm{Cat}$$
14	1 8 4 5 6 3 11	oppcsect	$$⊢\phi \to \left(G\left(X\mathrm{Sect}\left(\mathrm{oppCat}\left(C\right)\right)Y\right)F\leftrightarrow F\left(XSY\right)G\right)$$
15	7 14	mpbird	$$⊢\phi \to G\left(X\mathrm{Sect}\left(\mathrm{oppCat}\left(C\right)\right)Y\right)F$$
16	9 10 11 13 5 6 15	sectmon	$$⊢\phi \to G\in \left(X\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)Y\right)$$
17	8 4 10 2	oppcmon	$$⊢\phi \to X\mathrm{Mono}\left(\mathrm{oppCat}\left(C\right)\right)Y=YEX$$
18	16 17	eleqtrd	$$⊢\phi \to G\in \left(YEX\right)$$