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	\|- ( ph -> C e. Cat )
	sectepi.x	\|- ( ph -> X e. B )
	sectepi.y	\|- ( ph -> Y e. B )
	episect.n	\|- N = ( Inv ` C )
	episect.1	\|- ( ph -> F e. ( X E Y ) )
	episect.2	\|- ( ph -> F ( X S Y ) G )
Assertion	episect	\|- ( ph -> 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	\|- ( ph -> C e. Cat )
5		sectepi.x	\|- ( ph -> X e. B )
6		sectepi.y	\|- ( ph -> Y e. B )
7		episect.n	\|- N = ( Inv ` C )
8		episect.1	\|- ( ph -> F e. ( X E Y ) )
9		episect.2	\|- ( ph -> 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	\|- ( ph -> ( 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 e. Cat -> ( oppCat ` C ) e. Cat )
17	4 16	syl	\|- ( ph -> ( oppCat ` C ) e. Cat )
18	10 4 14 2	oppcmon	\|- ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) )
19	8 18	eleqtrrd	\|- ( ph -> F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) )
20	1 10 4 5 6 3 15	oppcsect	\|- ( ph -> ( G ( X ( Sect ` ( oppCat ` C ) ) Y ) F <-> F ( X S Y ) G ) )
21	9 20	mpbird	\|- ( ph -> G ( X ( Sect ` ( oppCat ` C ) ) Y ) F )
22	13 14 15 17 6 5 11 19 21	monsect	\|- ( ph -> F ( Y ( Inv ` ( oppCat ` C ) ) X ) G )
23	12 22	breqdi	\|- ( ph -> F ( X N Y ) G )

Metamath Proof Explorer

Theorem episect

Proof