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

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 episect.n 𝑁 = ( Inv ‘ 𝐶 )
8 episect.1 ( 𝜑𝐹 ∈ ( 𝑋 𝐸 𝑌 ) )
9 episect.2 ( 𝜑𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 )
10 eqid ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
11 eqid ( Inv ‘ ( oppCat ‘ 𝐶 ) ) = ( Inv ‘ ( oppCat ‘ 𝐶 ) )
12 1 10 4 6 5 7 11 oppcinv ( 𝜑 → ( 𝑌 ( Inv ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝑁 𝑌 ) )
13 10 1 oppcbas 𝐵 = ( Base ‘ ( oppCat ‘ 𝐶 ) )
14 eqid ( Mono ‘ ( oppCat ‘ 𝐶 ) ) = ( Mono ‘ ( oppCat ‘ 𝐶 ) )
15 eqid ( Sect ‘ ( oppCat ‘ 𝐶 ) ) = ( Sect ‘ ( oppCat ‘ 𝐶 ) )
16 10 oppccat ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ Cat )
17 4 16 syl ( 𝜑 → ( oppCat ‘ 𝐶 ) ∈ Cat )
18 10 4 14 2 oppcmon ( 𝜑 → ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) = ( 𝑋 𝐸 𝑌 ) )
19 8 18 eleqtrrd ( 𝜑𝐹 ∈ ( 𝑌 ( Mono ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) )
20 1 10 4 5 6 3 15 oppcsect ( 𝜑 → ( 𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹𝐹 ( 𝑋 𝑆 𝑌 ) 𝐺 ) )
21 9 20 mpbird ( 𝜑𝐺 ( 𝑋 ( Sect ‘ ( oppCat ‘ 𝐶 ) ) 𝑌 ) 𝐹 )
22 13 14 15 17 6 5 11 19 21 monsect ( 𝜑𝐹 ( 𝑌 ( Inv ‘ ( oppCat ‘ 𝐶 ) ) 𝑋 ) 𝐺 )
23 12 22 breqdi ( 𝜑𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )