Metamath Proof Explorer

Theorem fthsect

Description: A faithful functor reflects sections. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
fthsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
fthsect.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
fthsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
fthsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
fthsect.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
fthsect.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑋 ) )
fthsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
fthsect.t ⊢ 𝑇 = ( Sect ‘ 𝐷 )
Assertion fthsect ( 𝜑 → ( 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 fthsect.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 fthsect.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
3 fthsect.f ⊢ ( 𝜑 → 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 )
4 fthsect.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 fthsect.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6 fthsect.m ⊢ ( 𝜑 → 𝑀 ∈ ( 𝑋 𝐻 𝑌 ) )
7 fthsect.n ⊢ ( 𝜑 → 𝑁 ∈ ( 𝑌 𝐻 𝑋 ) )
8 fthsect.s ⊢ 𝑆 = ( Sect ‘ 𝐶 )
9 fthsect.t ⊢ 𝑇 = ( Sect ‘ 𝐷 )
10 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
11 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
12 fthfunc ⊢ ( 𝐶 Faith 𝐷 ) ⊆ ( 𝐶 Func 𝐷 )
13 12 ssbri ⊢ ( 𝐹 ( 𝐶 Faith 𝐷 ) 𝐺 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
14 3 13 syl ⊢ ( 𝜑 → 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 )
15 df-br ⊢ ( 𝐹 ( 𝐶 Func 𝐷 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
16 14 15 sylib ⊢ ( 𝜑 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) )
17 funcrcl ⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐶 Func 𝐷 ) → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
18 16 17 syl ⊢ ( 𝜑 → ( 𝐶 ∈ Cat ∧ 𝐷 ∈ Cat ) )
19 18 simpld ⊢ ( 𝜑 → 𝐶 ∈ Cat )
20 1 2 11 19 4 5 4 6 7 catcocl ⊢ ( 𝜑 → ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) ∈ ( 𝑋 𝐻 𝑋 ) )
21 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
22 1 2 21 19 4 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
23 1 2 10 3 4 4 20 22 fthi ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
24 eqid ⊢ ( comp ‘ 𝐷 ) = ( comp ‘ 𝐷 )
25 1 2 11 24 14 4 5 4 6 7 funcco ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) ) = ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) )
26 eqid ⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
27 1 21 26 14 4 funcid ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑋 ) ) )
28 25 27 eqeq12d ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑋 ) ‘ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) ) = ( ( 𝑋 𝐺 𝑋 ) ‘ ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) ↔ ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
29 23 28 bitr3d ⊢ ( 𝜑 → ( ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ↔ ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
30 1 2 11 21 8 19 4 5 6 7 issect2 ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 ↔ ( 𝑁 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑀 ) = ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) )
31 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
32 18 simprd ⊢ ( 𝜑 → 𝐷 ∈ Cat )
33 1 31 14 funcf1 ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝐷 ) )
34 33 4 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
35 33 5 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
36 1 2 10 14 4 5 funcf2 ⊢ ( 𝜑 → ( 𝑋 𝐺 𝑌 ) : ( 𝑋 𝐻 𝑌 ) ⟶ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
37 36 6 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ∈ ( ( 𝐹 ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑌 ) ) )
38 1 2 10 14 5 4 funcf2 ⊢ ( 𝜑 → ( 𝑌 𝐺 𝑋 ) : ( 𝑌 𝐻 𝑋 ) ⟶ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
39 38 7 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ∈ ( ( 𝐹 ‘ 𝑌 ) ( Hom ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) )
40 31 10 24 26 9 32 34 35 37 39 issect2 ⊢ ( 𝜑 → ( ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ↔ ( ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ( ⟨ ( 𝐹 ‘ 𝑋 ) , ( 𝐹 ‘ 𝑌 ) ⟩ ( comp ‘ 𝐷 ) ( 𝐹 ‘ 𝑋 ) ) ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ) = ( ( Id ‘ 𝐷 ) ‘ ( 𝐹 ‘ 𝑋 ) ) ) )
41 29 30 40 3bitr4d ⊢ ( 𝜑 → ( 𝑀 ( 𝑋 𝑆 𝑌 ) 𝑁 ↔ ( ( 𝑋 𝐺 𝑌 ) ‘ 𝑀 ) ( ( 𝐹 ‘ 𝑋 ) 𝑇 ( 𝐹 ‘ 𝑌 ) ) ( ( 𝑌 𝐺 𝑋 ) ‘ 𝑁 ) ) )