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 ⊢ 𝐵 = ( 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 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑌 𝐸 𝑋 ) )