Theorem monsect

Description: If F is a monomorphism and G is a section of F , then G is an inverse of F and they are both isomorphisms. This is also stated as "a monomorphism which is also a split epimorphism is an isomorphism". (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	sectmon.b	$$⊢B={\mathrm{Base}}_C$$
	sectmon.m	$$⊢M=\mathrm{Mono}\left(C\right)$$
	sectmon.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
	sectmon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	sectmon.x	$$⊢\phi \to X\in B$$
	sectmon.y	$$⊢\phi \to Y\in B$$
	monsect.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
	monsect.1	$$⊢\phi \to F\in \left(XMY\right)$$
	monsect.2	$$⊢\phi \to G\left(YSX\right)F$$
Assertion	monsect	$$⊢\phi \to F\left(XNY\right)G$$

Proof

Step	Hyp	Ref	Expression
1		sectmon.b	$$⊢B={\mathrm{Base}}_C$$
2		sectmon.m	$$⊢M=\mathrm{Mono}\left(C\right)$$
3		sectmon.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
4		sectmon.c	$$⊢\phi \to C\in \mathrm{Cat}$$
5		sectmon.x	$$⊢\phi \to X\in B$$
6		sectmon.y	$$⊢\phi \to Y\in B$$
7		monsect.n	$$⊢N=\mathrm{Inv}\left(C\right)$$
8		monsect.1	$$⊢\phi \to F\in \left(XMY\right)$$
9		monsect.2	$$⊢\phi \to G\left(YSX\right)F$$
10		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
11		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
12		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
13	1 10 11 12 3 4 6 5	issect	$$⊢\phi \to \left(G\left(YSX\right)F\leftrightarrow \left(G\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge F\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)G=\mathrm{Id}\left(C\right)\left(Y\right)\right)\right)$$
14	9 13	mpbid	$$⊢\phi \to \left(G\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge F\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)G=\mathrm{Id}\left(C\right)\left(Y\right)\right)$$
15	14	simp3d	$$⊢\phi \to F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)G=\mathrm{Id}\left(C\right)\left(Y\right)$$
16	15	oveq1d	$$⊢\phi \to \left(F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)G\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F$$
17	14	simp2d	$$⊢\phi \to F\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
18	14	simp1d	$$⊢\phi \to G\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
19	1 10 11 4 5 6 5 17 18 6 17	catass	$$⊢\phi \to \left(F\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)G\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F=F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\left(G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F\right)$$
20	1 10 12 4 5 11 6 17	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F=F$$
21	1 10 12 4 5 11 6 17	catrid	$$⊢\phi \to F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)=F$$
22	20 21	eqtr4d	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)F=F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)$$
23	16 19 22	3eqtr3d	$$⊢\phi \to F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\left(G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F\right)=F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)$$
24	1 10 11 4 5 6 5 17 18	catcocl	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
25	1 10 12 4 5	catidcl	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(X\right)\in \left(X\mathrm{Hom}\left(C\right)X\right)$$
26	1 10 11 2 4 5 6 5 8 24 25	moni	$$⊢\phi \to \left(F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\left(G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F\right)=F\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)\leftrightarrow G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
27	23 26	mpbid	$$⊢\phi \to G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F=\mathrm{Id}\left(C\right)\left(X\right)$$
28	1 10 11 12 3 4 5 6 17 18	issect2	$$⊢\phi \to \left(F\left(XSY\right)G\leftrightarrow G\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)F=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
29	27 28	mpbird	$$⊢\phi \to F\left(XSY\right)G$$
30	1 7 4 5 6 3	isinv	$$⊢\phi \to \left(F\left(XNY\right)G\leftrightarrow \left(F\left(XSY\right)G\wedge G\left(YSX\right)F\right)\right)$$
31	29 9 30	mpbir2and	$$⊢\phi \to F\left(XNY\right)G$$