Metamath Proof Explorer

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	$⊢ φ \to C \in Cat$
		sectepi.x	$⊢ φ \to X \in B$
		sectepi.y	$⊢ φ \to Y \in B$
		sectepi.1	$⊢ φ \to F (X S Y) G$
	Assertion	sectepi	$⊢ φ \to G \in (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	$⊢ φ \to C \in Cat$
5		sectepi.x	$⊢ φ \to X \in B$
6		sectepi.y	$⊢ φ \to Y \in B$
7		sectepi.1	$⊢ φ \to 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 \in Cat \to oppCat (C) \in Cat$
13	4 12	syl	$⊢ φ \to oppCat (C) \in Cat$
14	1 8 4 5 6 3 11	oppcsect	$⊢ φ \to (G (X Sect (oppCat (C)) Y) F \leftrightarrow F (X S Y) G)$
15	7 14	mpbird	$⊢ φ \to G (X Sect (oppCat (C)) Y) F$
16	9 10 11 13 5 6 15	sectmon	$⊢ φ \to G \in (X Mono (oppCat (C)) Y)$
17	8 4 10 2	oppcmon	$⊢ φ \to X Mono (oppCat (C)) Y = Y E X$
18	16 17	eleqtrd	$⊢ φ \to G \in (Y E X)$