Metamath Proof Explorer

Theorem cvmliftlem8

Description: Lemma for cvmlift . The functions Q are continuous functions because they are defined as ` ``' ( F |`I ) o. G where G is continuous and ` ( F |`I ) is a homeomorphism. (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
cvmliftlem5.3 ⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
Assertion cvmliftlem8 ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 ⊢ 𝑆 = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
2 cvmliftlem.b ⊢ 𝐵 = ∪ 𝐶
3 cvmliftlem.x ⊢ 𝑋 = ∪ 𝐽
4 cvmliftlem.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftlem.g ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
6 cvmliftlem.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
7 cvmliftlem.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
8 cvmliftlem.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
9 cvmliftlem.t ⊢ ( 𝜑 → 𝑇 : ( 1 ... 𝑁 ) ⟶ ∪ 𝑗 ∈ 𝐽 ( { 𝑗 } × ( 𝑆 ‘ 𝑗 ) ) )
10 cvmliftlem.a ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝐺 “ ( ( ( 𝑘 − 1 ) / 𝑁 ) [,] ( 𝑘 / 𝑁 ) ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑘 ) ) )
11 cvmliftlem.l ⊢ 𝐿 = ( topGen ‘ ran (,) )
12 cvmliftlem.q ⊢ 𝑄 = seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) )
13 cvmliftlem5.3 ⊢ 𝑊 = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) )
14 elfznn ⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ∈ ℕ )
15 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem5 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
16 14 15 sylan2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
17 4 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
18 cvmtop1 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐶 ∈ Top )
19 cnrest2r ⊢ ( 𝐶 ∈ Top → ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ) ⊆ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐶 ) )
20 17 18 19 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ) ⊆ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐶 ) )
21 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
22 11 21 eqeltri ⊢ 𝐿 ∈ ( TopOn ‘ ℝ )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
24 1 2 3 4 5 6 7 8 9 10 11 23 13 cvmliftlem2 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑊 ⊆ ( 0 [,] 1 ) )
25 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
26 24 25 sstrdi ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑊 ⊆ ℝ )
27 resttopon ⊢ ( ( 𝐿 ∈ ( TopOn ‘ ℝ ) ∧ 𝑊 ⊆ ℝ ) → ( 𝐿 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) )
28 22 26 27 sylancr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐿 ↾t 𝑊 ) ∈ ( TopOn ‘ 𝑊 ) )
29 eqid ⊢ ( II ↾t 𝑊 ) = ( II ↾t 𝑊 )
30 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
32 5 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
33 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
34 33 3 cnf ⊢ ( 𝐺 ∈ ( II Cn 𝐽 ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
35 32 34 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐺 : ( 0 [,] 1 ) ⟶ 𝑋 )
36 35 feqmptd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐺 = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ 𝑧 ) ) )
37 36 32 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( II Cn 𝐽 ) )
38 29 31 24 37 cnmpt1res ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( II ↾t 𝑊 ) Cn 𝐽 ) )
39 dfii2 ⊢ II = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
40 11 oveq1i ⊢ ( 𝐿 ↾t ( 0 [,] 1 ) ) = ( ( topGen ‘ ran (,) ) ↾t ( 0 [,] 1 ) )
41 39 40 eqtr4i ⊢ II = ( 𝐿 ↾t ( 0 [,] 1 ) )
42 41 oveq1i ⊢ ( II ↾t 𝑊 ) = ( ( 𝐿 ↾t ( 0 [,] 1 ) ) ↾t 𝑊 )
43 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
44 11 43 eqeltri ⊢ 𝐿 ∈ Top
45 44 a1i ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐿 ∈ Top )
46 ovexd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 0 [,] 1 ) ∈ V )
47 restabs ⊢ ( ( 𝐿 ∈ Top ∧ 𝑊 ⊆ ( 0 [,] 1 ) ∧ ( 0 [,] 1 ) ∈ V ) → ( ( 𝐿 ↾t ( 0 [,] 1 ) ) ↾t 𝑊 ) = ( 𝐿 ↾t 𝑊 ) )
48 45 24 46 47 syl3anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐿 ↾t ( 0 [,] 1 ) ) ↾t 𝑊 ) = ( 𝐿 ↾t 𝑊 ) )
49 42 48 eqtrid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( II ↾t 𝑊 ) = ( 𝐿 ↾t 𝑊 ) )
50 49 oveq1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( II ↾t 𝑊 ) Cn 𝐽 ) = ( ( 𝐿 ↾t 𝑊 ) Cn 𝐽 ) )
51 38 50 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐽 ) )
52 cvmtop2 ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐽 ∈ Top )
53 17 52 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐽 ∈ Top )
54 3 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
55 53 54 sylib ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
56 simprl ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝑊 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
57 simprr ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝑊 ) ) → 𝑧 ∈ 𝑊 )
58 1 2 3 4 5 6 7 8 9 10 11 56 13 57 cvmliftlem3 ⊢ ( ( 𝜑 ∧ ( 𝑀 ∈ ( 1 ... 𝑁 ) ∧ 𝑧 ∈ 𝑊 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
59 58 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝑊 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
60 59 fmpttd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) : 𝑊 ⟶ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
61 60 frnd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ran ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
62 1 2 3 4 5 6 7 8 9 10 11 23 cvmliftlem1 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) )
63 1 cvmsrcl ⊢ ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐽 )
64 elssuni ⊢ ( ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ 𝐽 → ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ ∪ 𝐽 )
65 62 63 64 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ ∪ 𝐽 )
66 65 3 sseqtrrdi ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ 𝑋 )
67 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ran ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ⊆ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ⊆ 𝑋 ) → ( ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐽 ) ↔ ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) ) )
68 55 61 66 67 syl3anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐽 ) ↔ ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) ) )
69 51 68 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( 𝐺 ‘ 𝑧 ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) )
70 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem7 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
71 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
72 2 3 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
73 17 71 72 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝐹 : 𝐵 ⟶ 𝑋 )
74 ffn ⊢ ( 𝐹 : 𝐵 ⟶ 𝑋 → 𝐹 Fn 𝐵 )
75 fniniseg ⊢ ( 𝐹 Fn 𝐵 → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
76 73 74 75 3syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ) )
77 70 76 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) )
78 77 simpld ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 )
79 77 simprd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
80 14 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ℕ )
81 80 nnred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ℝ )
82 peano2rem ⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
83 81 82 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ℝ )
84 8 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℕ )
85 83 84 nndivred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ )
86 85 rexrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* )
87 81 84 nndivred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ )
88 87 rexrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 / 𝑁 ) ∈ ℝ* )
89 81 ltm1d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) < 𝑀 )
90 84 nnred ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℝ )
91 84 nngt0d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 0 < 𝑁 )
92 ltdiv1 ⊢ ( ( ( 𝑀 − 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
93 83 81 90 91 92 syl112anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) < 𝑀 ↔ ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) ) )
94 89 93 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) < ( 𝑀 / 𝑁 ) )
95 85 87 94 ltled ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) )
96 lbicc2 ⊢ ( ( ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑀 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑀 − 1 ) / 𝑁 ) ≤ ( 𝑀 / 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
97 86 88 95 96 syl3anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
98 97 13 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑀 − 1 ) / 𝑁 ) ∈ 𝑊 )
99 1 2 3 4 5 6 7 8 9 10 11 23 13 98 cvmliftlem3 ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
100 79 99 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) )
101 eqid ⊢ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 )
102 1 2 101 cvmsiota ⊢ ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ) ∈ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
103 17 62 78 100 102 syl13anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∧ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
104 103 simpld ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) )
105 1 cvmshmeo ⊢ ( ( ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ∈ ( 𝑆 ‘ ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ∧ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) Homeo ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) )
106 62 104 105 syl2anc ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) Homeo ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) )
107 hmeocnvcn ⊢ ( ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ∈ ( ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) Homeo ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ∈ ( ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) Cn ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ) )
108 106 107 syl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ∈ ( ( 𝐽 ↾t ( 1st ‘ ( 𝑇 ‘ 𝑀 ) ) ) Cn ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ) )
109 28 69 108 cnmpt11f ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn ( 𝐶 ↾t ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ) )
110 20 109 sseldd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐶 ) )
111 16 110 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 𝑀 ) ∈ ( ( 𝐿 ↾t 𝑊 ) Cn 𝐶 ) )