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	⊢ 𝐵 = ( Base ‘ 𝐶 )
	sectepi.e	⊢ 𝐸 = ( Epi ‘ 𝐶 )
	sectepi.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
	sectepi.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	sectepi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	sectepi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	sectepi.1	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
Assertion	sectepi	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐸 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		sectepi.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		sectepi.e	⊢ 𝐸 = ( Epi ‘ 𝐶 )
3		sectepi.s	⊢ 𝑆 = ( Sect ‘ 𝐶 )
4		sectepi.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
5		sectepi.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		sectepi.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		sectepi.1	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
8		eqid	⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
9	8 1	oppcbas	⊢ 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
10		eqid	⊢ ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) )
11		eqid	⊢ ( Sect ‘ ( oppCat ‘ 𝐶 ) ) = ( Sect ‘ ( oppCat ‘ 𝐶 ) )
12	8	oppccat	⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
13	4 12	syl	⊢ ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
14	1 8 4 5 6 3 11	oppcsect	⊢ ( 𝜑 → ( 𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹 ↔ 𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) )
15	7 14	mpbird	⊢ ( 𝜑 → 𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹 )
16	9 10 11 13 5 6 15	sectmon	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) )
17	8 4 10 2	oppcmon	⊢ ( 𝜑 → ( 𝑋 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) = ( 𝑌 𝐸 𝑋 ) )
18	16 17	eleqtrd	⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐸 𝑋 ) )