Metamath Proof Explorer

Theorem cvmliftlem7

Description: Lemma for cvmlift . Prove by induction that every Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 to show functionality and lifting of Q ). (Contributed by Mario Carneiro, 14-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 cvmliftlem7 ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )

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 fzssp1 ⊢ ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... ( ( 𝑁 − 1 ) + 1 ) )
15 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑁 ∈ ℂ )
17 ax-1cn ⊢ 1 ∈ ℂ
18 npcan ⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
19 16 17 18 sylancl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 0 ... ( ( 𝑁 − 1 ) + 1 ) ) = ( 0 ... 𝑁 ) )
21 14 20 sseqtrid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ( 1 ... 𝑁 ) )
23 elfzelz ⊢ ( 𝑀 ∈ ( 1 ... 𝑁 ) → 𝑀 ∈ ℤ )
24 8 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
25 elfzm1b ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
26 23 24 25 syl2anr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) ) )
27 22 26 mpbid ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
28 21 27 sseldd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) )
29 elfznn0 ⊢ ( ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑀 − 1 ) ∈ ℕ0 )
30 29 adantl ⊢ ( ( 𝜑 ∧ ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) ) → ( 𝑀 − 1 ) ∈ ℕ0 )
31 eleq1 ⊢ ( 𝑦 = 0 → ( 𝑦 ∈ ( 0 ... 𝑁 ) ↔ 0 ∈ ( 0 ... 𝑁 ) ) )
32 fveq2 ⊢ ( 𝑦 = 0 → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 0 ) )
33 oveq1 ⊢ ( 𝑦 = 0 → ( 𝑦 / 𝑁 ) = ( 0 / 𝑁 ) )
34 32 33 fveq12d ⊢ ( 𝑦 = 0 → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) = ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) )
35 fvoveq1 ⊢ ( 𝑦 = 0 → ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) = ( 𝐺 ‘ ( 0 / 𝑁 ) ) )
36 35 sneqd ⊢ ( 𝑦 = 0 → { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } = { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } )
37 36 imaeq2d ⊢ ( 𝑦 = 0 → ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) = ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) )
38 34 37 eleq12d ⊢ ( 𝑦 = 0 → ( ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ↔ ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ) )
39 31 38 imbi12d ⊢ ( 𝑦 = 0 → ( ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ↔ ( 0 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ) ) )
40 39 imbi2d ⊢ ( 𝑦 = 0 → ( ( 𝜑 → ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ) ↔ ( 𝜑 → ( 0 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ) ) ) )
41 eleq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 ∈ ( 0 ... 𝑁 ) ↔ 𝑛 ∈ ( 0 ... 𝑁 ) ) )
42 fveq2 ⊢ ( 𝑦 = 𝑛 → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑛 ) )
43 oveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 / 𝑁 ) = ( 𝑛 / 𝑁 ) )
44 42 43 fveq12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) = ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) )
45 fvoveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) = ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) )
46 45 sneqd ⊢ ( 𝑦 = 𝑛 → { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } = { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } )
47 46 imaeq2d ⊢ ( 𝑦 = 𝑛 → ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) = ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) )
48 44 47 eleq12d ⊢ ( 𝑦 = 𝑛 → ( ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ↔ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) )
49 41 48 imbi12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ↔ ( 𝑛 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) )
50 49 imbi2d ⊢ ( 𝑦 = 𝑛 → ( ( 𝜑 → ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) ) )
51 eleq1 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝑦 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) )
52 fveq2 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
53 oveq1 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝑦 / 𝑁 ) = ( ( 𝑛 + 1 ) / 𝑁 ) )
54 52 53 fveq12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
55 fvoveq1 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
56 55 sneqd ⊢ ( 𝑦 = ( 𝑛 + 1 ) → { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } = { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } )
57 56 imaeq2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) = ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) )
58 54 57 eleq12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ↔ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ) )
59 51 58 imbi12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ) ) )
60 59 imbi2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ) ) ) )
61 eleq1 ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝑦 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) ) )
62 fveq2 ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ ( 𝑀 − 1 ) ) )
63 oveq1 ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝑦 / 𝑁 ) = ( ( 𝑀 − 1 ) / 𝑁 ) )
64 62 63 fveq12d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
65 fvoveq1 ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
66 65 sneqd ⊢ ( 𝑦 = ( 𝑀 − 1 ) → { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } = { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } )
67 66 imaeq2d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) = ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
68 64 67 eleq12d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ↔ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ) )
69 61 68 imbi12d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ↔ ( ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ) ) )
70 69 imbi2d ⊢ ( 𝑦 = ( 𝑀 − 1 ) → ( ( 𝜑 → ( 𝑦 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑦 ) ‘ ( 𝑦 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑦 / 𝑁 ) ) } ) ) ) ↔ ( 𝜑 → ( ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ) ) ) )
71 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem4 ⊢ ( 𝑄 ‘ 0 ) = { ⟨ 0 , 𝑃 ⟩ }
72 71 a1i ⊢ ( 𝜑 → ( 𝑄 ‘ 0 ) = { ⟨ 0 , 𝑃 ⟩ } )
73 8 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
74 15 73 div0d ⊢ ( 𝜑 → ( 0 / 𝑁 ) = 0 )
75 72 74 fveq12d ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) = ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) )
76 0nn0 ⊢ 0 ∈ ℕ0
77 fvsng ⊢ ( ( 0 ∈ ℕ0 ∧ 𝑃 ∈ 𝐵 ) → ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) = 𝑃 )
78 76 6 77 sylancr ⊢ ( 𝜑 → ( { ⟨ 0 , 𝑃 ⟩ } ‘ 0 ) = 𝑃 )
79 75 78 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) = 𝑃 )
80 74 fveq2d ⊢ ( 𝜑 → ( 𝐺 ‘ ( 0 / 𝑁 ) ) = ( 𝐺 ‘ 0 ) )
81 7 80 eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ ( 0 / 𝑁 ) ) )
82 cvmcn ⊢ ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
83 4 82 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Cn 𝐽 ) )
84 2 3 cnf ⊢ ( 𝐹 ∈ ( 𝐶 Cn 𝐽 ) → 𝐹 : 𝐵 ⟶ 𝑋 )
85 ffn ⊢ ( 𝐹 : 𝐵 ⟶ 𝑋 → 𝐹 Fn 𝐵 )
86 83 84 85 3syl ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
87 fniniseg ⊢ ( 𝐹 Fn 𝐵 → ( 𝑃 ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ↔ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ ( 0 / 𝑁 ) ) ) ) )
88 86 87 syl ⊢ ( 𝜑 → ( 𝑃 ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ↔ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ ( 0 / 𝑁 ) ) ) ) )
89 6 81 88 mpbir2and ⊢ ( 𝜑 → 𝑃 ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) )
90 79 89 eqeltrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) )
91 90 a1d ⊢ ( 𝜑 → ( 0 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 0 ) ‘ ( 0 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 0 / 𝑁 ) ) } ) ) )
92 id ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ℕ0 )
93 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
94 92 93 eleqtrdi ⊢ ( 𝑛 ∈ ℕ0 → 𝑛 ∈ ( ℤ≥ ‘ 0 ) )
95 94 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → 𝑛 ∈ ( ℤ≥ ‘ 0 ) )
96 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 0 ) ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) → 𝑛 ∈ ( 0 ... 𝑁 ) )
97 96 ex ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 0 ) → ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ( 0 ... 𝑁 ) ) )
98 95 97 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → 𝑛 ∈ ( 0 ... 𝑁 ) ) )
99 98 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ0 ) → ( ( 𝑛 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) → ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) )
100 eqid ⊢ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) )
101 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) )
102 elfzle2 ⊢ ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑛 + 1 ) ≤ 𝑁 )
103 101 102 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ≤ 𝑁 )
104 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑛 ∈ ℕ0 )
105 nn0p1nn ⊢ ( 𝑛 ∈ ℕ0 → ( 𝑛 + 1 ) ∈ ℕ )
106 104 105 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
107 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
108 106 107 eleqtrdi ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
109 24 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑁 ∈ ℤ )
110 elfz5 ⊢ ( ( ( 𝑛 + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ≤ 𝑁 ) )
111 108 109 110 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ≤ 𝑁 ) )
112 103 111 mpbird ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) )
113 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) )
114 104 nn0cnd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑛 ∈ ℂ )
115 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
116 114 17 115 sylancl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
117 116 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑄 ‘ 𝑛 ) )
118 116 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) = ( 𝑛 / 𝑁 ) )
119 117 118 fveq12d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) )
120 118 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝐺 ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) )
121 120 sneqd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → { ( 𝐺 ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) } = { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } )
122 121 imaeq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) } ) = ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) )
123 113 119 122 3eltr4d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) } ) )
124 1 2 3 4 5 6 7 8 9 10 11 12 100 112 123 cvmliftlem6 ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
125 124 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 )
126 104 nn0red ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑛 ∈ ℝ )
127 8 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑁 ∈ ℕ )
128 126 127 nndivred ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 / 𝑁 ) ∈ ℝ )
129 128 rexrd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 / 𝑁 ) ∈ ℝ* )
130 peano2re ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 + 1 ) ∈ ℝ )
131 126 130 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 + 1 ) ∈ ℝ )
132 131 127 nndivred ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ )
133 132 rexrd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* )
134 126 ltp1d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑛 < ( 𝑛 + 1 ) )
135 127 nnred ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝑁 ∈ ℝ )
136 127 nngt0d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 0 < 𝑁 )
137 ltdiv1 ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑛 + 1 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 𝑛 < ( 𝑛 + 1 ) ↔ ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) ) )
138 126 131 135 136 137 syl112anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 < ( 𝑛 + 1 ) ↔ ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) ) )
139 134 138 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) )
140 128 132 139 ltled ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) )
141 ubicc2 ⊢ ( ( ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
142 129 133 140 141 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
143 118 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
144 142 143 eleqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
145 125 144 ffvelcdmd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ 𝐵 )
146 124 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
147 143 reseq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
148 146 147 eqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
149 148 fveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
150 143 feq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ↔ ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ) )
151 125 150 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 )
152 fvco3 ⊢ ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) → ( ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
153 151 142 152 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
154 fvres ⊢ ( ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) → ( ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
155 142 154 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
156 149 153 155 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) )
157 86 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → 𝐹 Fn 𝐵 )
158 fniniseg ⊢ ( 𝐹 Fn 𝐵 → ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
159 157 158 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ↔ ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ 𝐵 ∧ ( 𝐹 ‘ ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
160 145 156 159 mpbir2and ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ∧ ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) )
161 160 expr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ0 ∧ ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) ) ) → ( ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ) )
162 99 161 animpimp2impd ⊢ ( 𝑛 ∈ ℕ0 → ( ( 𝜑 → ( 𝑛 ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( 𝑛 / 𝑁 ) ) } ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 + 1 ) / 𝑁 ) ) } ) ) ) ) )
163 40 50 60 70 91 162 nn0ind ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( 𝜑 → ( ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ) ) )
164 163 impd ⊢ ( ( 𝑀 − 1 ) ∈ ℕ0 → ( ( 𝜑 ∧ ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) ) )
165 30 164 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑀 − 1 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )
166 28 165 syldan ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) } ) )