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 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 ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹𝑋 ) 𝑇 ( 𝐹𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) )