Theorem sectcan

Description: If G is a section of F and F is a section of H , then G = H . Proposition 3.10 of Adamek p. 28. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	sectcan.b	$$⊢B={\mathrm{Base}}_C$$
	sectcan.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
	sectcan.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	sectcan.x	$$⊢\phi \to X\in B$$
	sectcan.y	$$⊢\phi \to Y\in B$$
	sectcan.1	$$⊢\phi \to G\left(XSY\right)F$$
	sectcan.2	$$⊢\phi \to F\left(YSX\right)H$$
Assertion	sectcan	$$⊢\phi \to G=H$$

Proof

Step	Hyp	Ref	Expression
1		sectcan.b	$$⊢B={\mathrm{Base}}_C$$
2		sectcan.s	$$⊢S=\mathrm{Sect}\left(C\right)$$
3		sectcan.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		sectcan.x	$$⊢\phi \to X\in B$$
5		sectcan.y	$$⊢\phi \to Y\in B$$
6		sectcan.1	$$⊢\phi \to G\left(XSY\right)F$$
7		sectcan.2	$$⊢\phi \to F\left(YSX\right)H$$
8		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
9		eqid	$$⊢\mathrm{comp}\left(C\right)=\mathrm{comp}\left(C\right)$$
10		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
11	1 8 9 10 2 3 4 5	issect	$$⊢\phi \to \left(G\left(XSY\right)F\leftrightarrow \left(G\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge F\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge F\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)G=\mathrm{Id}\left(C\right)\left(X\right)\right)\right)$$
12	6 11	mpbid	$$⊢\phi \to \left(G\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge F\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge F\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)G=\mathrm{Id}\left(C\right)\left(X\right)\right)$$
13	12	simp1d	$$⊢\phi \to G\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
14	1 8 9 10 2 3 5 4	issect	$$⊢\phi \to \left(F\left(YSX\right)H\leftrightarrow \left(F\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge H\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge H\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)\right)\right)$$
15	7 14	mpbid	$$⊢\phi \to \left(F\in \left(Y\mathrm{Hom}\left(C\right)X\right)\wedge H\in \left(X\mathrm{Hom}\left(C\right)Y\right)\wedge H\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)\right)$$
16	15	simp1d	$$⊢\phi \to F\in \left(Y\mathrm{Hom}\left(C\right)X\right)$$
17	15	simp2d	$$⊢\phi \to H\in \left(X\mathrm{Hom}\left(C\right)Y\right)$$
18	1 8 9 3 4 5 4 13 16 5 17	catass	$$⊢\phi \to \left(H\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)G=H\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\left(F\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)G\right)$$
19	15	simp3d	$$⊢\phi \to H\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F=\mathrm{Id}\left(C\right)\left(Y\right)$$
20	19	oveq1d	$$⊢\phi \to \left(H\left(⟨Y,X⟩\mathrm{comp}\left(C\right)Y\right)F\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)G=\mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)G$$
21	12	simp3d	$$⊢\phi \to F\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)G=\mathrm{Id}\left(C\right)\left(X\right)$$
22	21	oveq2d	$$⊢\phi \to H\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\left(F\left(⟨X,Y⟩\mathrm{comp}\left(C\right)X\right)G\right)=H\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)$$
23	18 20 22	3eqtr3d	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)G=H\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)$$
24	1 8 10 3 4 9 5 13	catlid	$$⊢\phi \to \mathrm{Id}\left(C\right)\left(Y\right)\left(⟨X,Y⟩\mathrm{comp}\left(C\right)Y\right)G=G$$
25	1 8 10 3 4 9 5 17	catrid	$$⊢\phi \to H\left(⟨X,X⟩\mathrm{comp}\left(C\right)Y\right)\mathrm{Id}\left(C\right)\left(X\right)=H$$
26	23 24 25	3eqtr3d	$$⊢\phi \to G=H$$