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	⊢ ( 𝜑 → 𝐹 ( 𝑋 𝑁 𝑌 ) 𝐺 )

Metamath Proof Explorer

Theorem episect

Proof