Metamath Proof Explorer

Theorem episect

Description: If F is an epimorphism and F is a section of G , then G is an inverse of F and they are both isomorphisms. This is also stated as "an epimorphism which is also a split monomorphism is an isomorphism". (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
episect.n ⊢ N = Inv ⁡ C
episect.1 ⊢ φ → F ∈ X E Y
episect.2 ⊢ φ → F X S Y G
Assertion episect ⊢ φ → F X N Y G

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 episect.n ⊢ N = Inv ⁡ C
8 episect.1 ⊢ φ → F ∈ X E Y
9 episect.2 ⊢ φ → F X S Y G
10 eqid ⊢ oppCat ⁡ C = oppCat ⁡ C
11 eqid ⊢ Inv ⁡ oppCat ⁡ C = Inv ⁡ oppCat ⁡ C
12 1 10 4 6 5 7 11 oppcinv ⊢ φ → Y Inv ⁡ oppCat ⁡ C X = X N Y
13 10 1 oppcbas ⊢ B = Base oppCat ⁡ C
14 eqid ⊢ Mono ⁡ oppCat ⁡ C = Mono ⁡ oppCat ⁡ C
15 eqid ⊢ Sect ⁡ oppCat ⁡ C = Sect ⁡ oppCat ⁡ C
16 10 oppccat ⊢ C ∈ Cat → oppCat ⁡ C ∈ Cat
17 4 16 syl ⊢ φ → oppCat ⁡ C ∈ Cat
18 10 4 14 2 oppcmon ⊢ φ → Y Mono ⁡ oppCat ⁡ C X = X E Y
19 8 18 eleqtrrd ⊢ φ → F ∈ Y Mono ⁡ oppCat ⁡ C X
20 1 10 4 5 6 3 15 oppcsect ⊢ φ → G X Sect ⁡ oppCat ⁡ C Y F ↔ F X S Y G
21 9 20 mpbird ⊢ φ → G X Sect ⁡ oppCat ⁡ C Y F
22 13 14 15 17 6 5 11 19 21 monsect ⊢ φ → F Y Inv ⁡ oppCat ⁡ C X G
23 12 22 breqdi ⊢ φ → F X N Y G