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	⊢ 𝐵 = ( Base ‘ 𝐷 )
	funcsect.s	⊢ 𝑆 = ( Sect ‘ 𝐷 )
	funcsect.t	⊢ 𝑇 = ( Sect ‘ 𝐸 )
	funcsect.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
	funcsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	funcsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	funcsect.m	⊢ ( 𝜑 → 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 )
Assertion	funcsect	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		funcsect.b	⊢ 𝐵 = ( Base ‘ 𝐷 )
2		funcsect.s	⊢ 𝑆 = ( Sect ‘ 𝐷 )
3		funcsect.t	⊢ 𝑇 = ( Sect ‘ 𝐸 )
4		funcsect.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
5		funcsect.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6		funcsect.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
7		funcsect.m	⊢ ( 𝜑 → 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9		eqid	⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
10		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
11		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
12	4 11	sylib	⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
13		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
14	12 13	syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
15	14	simpld	⊢ ( 𝜑 → 𝐷 ∈ Cat )
16	1 8 9 10 2 15 5 6	issect	⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 ↔ ( 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) ∧ 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑋 ) ∧ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) ) )
17	7 16	mpbid	⊢ ( 𝜑 → ( 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) ∧ 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑋 ) ∧ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) )
18	17	simp3d	⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) )
19	18	fveq2d	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑀 ) ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) )
20		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
21	17	simp1d	⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) )
22	17	simp2d	⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 ( Hom ‘ 𝐷 ) 𝑋 ) )
23	1 8 9 20 4 5 6 5 21 22	funcco	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐷 ) 𝑋 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )
24		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
25	1 10 24 4 5	funcid	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐷 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
26	19 23 25	3eqtr3d	⊢ ( 𝜑 → ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
27		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
28		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
29	14	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )
30	1 27 4	funcf1	⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐸 ) )
31	30 5	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
32	30 6	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐸 ) )
33	1 8 28 4 5 6	funcf2	⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
34	33 21	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
35	1 8 28 4 6 5	funcf2	⊢ ( 𝜑 → ( 𝑌 𝐺 𝑋 ) : ( 𝑌 ( Hom ‘ 𝐷 ) 𝑋 ) ⟶ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
36	35 22	ffvelrnd	⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
37	27 28 20 24 3 29 31 32 34 36	issect2	⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ↔ ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
38	26 37	mpbird	⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )