Theorem funcsect

Description: The image of a section under a functor is a section. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	funcsect.b	$$⊢B={\mathrm{Base}}_D$$
	funcsect.s	$$⊢S=\mathrm{Sect}\left(D\right)$$
	funcsect.t	$$⊢T=\mathrm{Sect}\left(E\right)$$
	funcsect.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
	funcsect.x	$$⊢\phi \to X\in B$$
	funcsect.y	$$⊢\phi \to Y\in B$$
	funcsect.m	$$⊢\phi \to M\left(XSY\right)N$$
Assertion	funcsect	$$⊢\phi \to \left(XGY\right)\left(M\right)\left(F\left(X\right)TF\left(Y\right)\right)\left(YGX\right)\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcsect.b	$$⊢B={\mathrm{Base}}_D$$
2		funcsect.s	$$⊢S=\mathrm{Sect}\left(D\right)$$
3		funcsect.t	$$⊢T=\mathrm{Sect}\left(E\right)$$
4		funcsect.f	$$⊢\phi \to F\left(D\mathrm{Func}E\right)G$$
5		funcsect.x	$$⊢\phi \to X\in B$$
6		funcsect.y	$$⊢\phi \to Y\in B$$
7		funcsect.m	$$⊢\phi \to M\left(XSY\right)N$$
8		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
9		eqid	$$⊢\mathrm{comp}\left(D\right)=\mathrm{comp}\left(D\right)$$
10		eqid	$$⊢\mathrm{Id}\left(D\right)=\mathrm{Id}\left(D\right)$$
11		df-br	$$⊢F\left(D\mathrm{Func}E\right)G\leftrightarrow ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
12	4 11	sylib	$$⊢\phi \to ⟨F,G⟩\in \left(D\mathrm{Func}E\right)$$
13		funcrcl	$$⊢⟨F,G⟩\in \left(D\mathrm{Func}E\right)\to \left(D\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
14	12 13	syl	$$⊢\phi \to \left(D\in \mathrm{Cat}\wedge E\in \mathrm{Cat}\right)$$
15	14	simpld	$$⊢\phi \to D\in \mathrm{Cat}$$
16	1 8 9 10 2 15 5 6	issect	$$⊢\phi \to \left(M\left(XSY\right)N\leftrightarrow \left(M\in \left(X\mathrm{Hom}\left(D\right)Y\right)\wedge N\in \left(Y\mathrm{Hom}\left(D\right)X\right)\wedge N\left(⟨X,Y⟩\mathrm{comp}\left(D\right)X\right)M=\mathrm{Id}\left(D\right)\left(X\right)\right)\right)$$
17	7 16	mpbid	$$⊢\phi \to \left(M\in \left(X\mathrm{Hom}\left(D\right)Y\right)\wedge N\in \left(Y\mathrm{Hom}\left(D\right)X\right)\wedge N\left(⟨X,Y⟩\mathrm{comp}\left(D\right)X\right)M=\mathrm{Id}\left(D\right)\left(X\right)\right)$$
18	17	simp3d	$$⊢\phi \to N\left(⟨X,Y⟩\mathrm{comp}\left(D\right)X\right)M=\mathrm{Id}\left(D\right)\left(X\right)$$
19	18	fveq2d	$$⊢\phi \to \left(XGX\right)\left(N\left(⟨X,Y⟩\mathrm{comp}\left(D\right)X\right)M\right)=\left(XGX\right)\left(\mathrm{Id}\left(D\right)\left(X\right)\right)$$
20		eqid	$$⊢\mathrm{comp}\left(E\right)=\mathrm{comp}\left(E\right)$$
21	17	simp1d	$$⊢\phi \to M\in \left(X\mathrm{Hom}\left(D\right)Y\right)$$
22	17	simp2d	$$⊢\phi \to N\in \left(Y\mathrm{Hom}\left(D\right)X\right)$$
23	1 8 9 20 4 5 6 5 21 22	funcco	$$⊢\phi \to \left(XGX\right)\left(N\left(⟨X,Y⟩\mathrm{comp}\left(D\right)X\right)M\right)=\left(YGX\right)\left(N\right)\left(⟨F\left(X\right),F\left(Y\right)⟩\mathrm{comp}\left(E\right)F\left(X\right)\right)\left(XGY\right)\left(M\right)$$
24		eqid	$$⊢\mathrm{Id}\left(E\right)=\mathrm{Id}\left(E\right)$$
25	1 10 24 4 5	funcid	$$⊢\phi \to \left(XGX\right)\left(\mathrm{Id}\left(D\right)\left(X\right)\right)=\mathrm{Id}\left(E\right)\left(F\left(X\right)\right)$$
26	19 23 25	3eqtr3d	$$⊢\phi \to \left(YGX\right)\left(N\right)\left(⟨F\left(X\right),F\left(Y\right)⟩\mathrm{comp}\left(E\right)F\left(X\right)\right)\left(XGY\right)\left(M\right)=\mathrm{Id}\left(E\right)\left(F\left(X\right)\right)$$
27		eqid	$$⊢{\mathrm{Base}}_E={\mathrm{Base}}_E$$
28		eqid	$$⊢\mathrm{Hom}\left(E\right)=\mathrm{Hom}\left(E\right)$$
29	14	simprd	$$⊢\phi \to E\in \mathrm{Cat}$$
30	1 27 4	funcf1	$$⊢\phi \to F:B⟶{\mathrm{Base}}_E$$
31	30 5	ffvelrnd	$$⊢\phi \to F\left(X\right)\in {\mathrm{Base}}_E$$
32	30 6	ffvelrnd	$$⊢\phi \to F\left(Y\right)\in {\mathrm{Base}}_E$$
33	1 8 28 4 5 6	funcf2	$$⊢\phi \to \left(XGY\right):X\mathrm{Hom}\left(D\right)Y⟶F\left(X\right)\mathrm{Hom}\left(E\right)F\left(Y\right)$$
34	33 21	ffvelrnd	$$⊢\phi \to \left(XGY\right)\left(M\right)\in \left(F\left(X\right)\mathrm{Hom}\left(E\right)F\left(Y\right)\right)$$
35	1 8 28 4 6 5	funcf2	$$⊢\phi \to \left(YGX\right):Y\mathrm{Hom}\left(D\right)X⟶F\left(Y\right)\mathrm{Hom}\left(E\right)F\left(X\right)$$
36	35 22	ffvelrnd	$$⊢\phi \to \left(YGX\right)\left(N\right)\in \left(F\left(Y\right)\mathrm{Hom}\left(E\right)F\left(X\right)\right)$$
37	27 28 20 24 3 29 31 32 34 36	issect2	$$⊢\phi \to \left(\left(XGY\right)\left(M\right)\left(F\left(X\right)TF\left(Y\right)\right)\left(YGX\right)\left(N\right)\leftrightarrow \left(YGX\right)\left(N\right)\left(⟨F\left(X\right),F\left(Y\right)⟩\mathrm{comp}\left(E\right)F\left(X\right)\right)\left(XGY\right)\left(M\right)=\mathrm{Id}\left(E\right)\left(F\left(X\right)\right)\right)$$
38	26 37	mpbird	$$⊢\phi \to \left(XGY\right)\left(M\right)\left(F\left(X\right)TF\left(Y\right)\right)\left(YGX\right)\left(N\right)$$