This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐸 ) )
32 30 6 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐸 ) )
33 1 8 28 4 5 6 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 ( Hom ‘ 𝐷 ) 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
34 33 21 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑌 ) ) )
35 1 8 28 4 6 5 funcf2 ⊢ ( 𝜑 → ( 𝑌 𝐺 𝑋 ) : ( 𝑌 ( Hom ‘ 𝐷 ) 𝑋 ) ⟶ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
36 35 22 ffvelcdmd ⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) )
37 27 28 20 24 3 29 31 32 34 36 issect2 ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ↔ ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐸 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
38 26 37 mpbird ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )