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 ⊢ B = Base C
sectepi.e ⊢ E = Epi ⁡ C
sectepi.s ⊢ S = Sect ⁡ C
sectepi.c ⊢ φ → C ∈ Cat
sectepi.x ⊢ φ → X ∈ B
sectepi.y ⊢ φ → Y ∈ B
sectepi.1 ⊢ φ → F X S Y G
Assertion sectepi ⊢ φ → G ∈ 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 ⊢ φ → C ∈ Cat
5 sectepi.x ⊢ φ → X ∈ B
6 sectepi.y ⊢ φ → Y ∈ B
7 sectepi.1 ⊢ φ → 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 ∈ Cat → oppCat ⁡ C ∈ Cat
13 4 12 syl ⊢ φ → oppCat ⁡ C ∈ Cat
14 1 8 4 5 6 3 11 oppcsect ⊢ φ → G X Sect ⁡ oppCat ⁡ C Y F ↔ F X S Y G
15 7 14 mpbird ⊢ φ → G X Sect ⁡ oppCat ⁡ C Y F
16 9 10 11 13 5 6 15 sectmon ⊢ φ → G ∈ X Mono ⁡ oppCat ⁡ C Y
17 8 4 10 2 oppcmon ⊢ φ → X Mono ⁡ oppCat ⁡ C Y = Y E X
18 16 17 eleqtrd ⊢ φ → G ∈ Y E X