Metamath Proof Explorer

Theorem cvmliftlem10

Description: Lemma for cvmlift . The function K is going to be our complete lifted path, formed by unioning together all the Q functions (each of which is defined on one segment [ ( M - 1 ) / N , M / N ] of the interval). Here we prove by induction that K is a continuous function and a lift of G by applying cvmliftlem6 , cvmliftlem7 (to show it is a function and a lift), cvmliftlem8 (to show it is continuous), and cvmliftlem9 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste gives that K is well-defined and continuous). (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 , 𝑃 ⟩ } ⟩ } ) )
cvmliftlem.k ⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
cvmliftlem10.1 ⊢ ( 𝜒 ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) )
Assertion cvmliftlem10 ( 𝜑 → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) )

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 cvmliftlem.k ⊢ 𝐾 = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 )
14 cvmliftlem10.1 ⊢ ( 𝜒 ↔ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) )
15 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
16 8 15 eleqtrdi ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
17 eluzfz2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 𝑁 ∈ ( 1 ... 𝑁 ) )
18 16 17 syl ⊢ ( 𝜑 → 𝑁 ∈ ( 1 ... 𝑁 ) )
19 eleq1 ⊢ ( 𝑦 = 1 → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ 1 ∈ ( 1 ... 𝑁 ) ) )
20 oveq2 ⊢ ( 𝑦 = 1 → ( 1 ... 𝑦 ) = ( 1 ... 1 ) )
21 1z ⊢ 1 ∈ ℤ
22 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
23 21 22 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
24 20 23 eqtrdi ⊢ ( 𝑦 = 1 → ( 1 ... 𝑦 ) = { 1 } )
25 24 iuneq1d ⊢ ( 𝑦 = 1 → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = ∪ 𝑘 ∈ { 1 } ( 𝑄 ‘ 𝑘 ) )
26 1ex ⊢ 1 ∈ V
27 fveq2 ⊢ ( 𝑘 = 1 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 1 ) )
28 26 27 iunxsn ⊢ ∪ 𝑘 ∈ { 1 } ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 1 )
29 25 28 eqtrdi ⊢ ( 𝑦 = 1 → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 1 ) )
30 oveq1 ⊢ ( 𝑦 = 1 → ( 𝑦 / 𝑁 ) = ( 1 / 𝑁 ) )
31 30 oveq2d ⊢ ( 𝑦 = 1 → ( 0 [,] ( 𝑦 / 𝑁 ) ) = ( 0 [,] ( 1 / 𝑁 ) ) )
32 31 oveq2d ⊢ ( 𝑦 = 1 → ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) )
33 32 oveq1d ⊢ ( 𝑦 = 1 → ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) )
34 29 33 eleq12d ⊢ ( 𝑦 = 1 → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ↔ ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ) )
35 29 coeq2d ⊢ ( 𝑦 = 1 → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) )
36 31 reseq2d ⊢ ( 𝑦 = 1 → ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) )
37 35 36 eqeq12d ⊢ ( 𝑦 = 1 → ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ↔ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) )
38 34 37 anbi12d ⊢ ( 𝑦 = 1 → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ↔ ( ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) ) )
39 19 38 imbi12d ⊢ ( 𝑦 = 1 → ( ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ↔ ( 1 ∈ ( 1 ... 𝑁 ) → ( ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) ) ) )
40 39 imbi2d ⊢ ( 𝑦 = 1 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ) ↔ ( 𝜑 → ( 1 ∈ ( 1 ... 𝑁 ) → ( ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) ) ) ) )
41 eleq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ 𝑛 ∈ ( 1 ... 𝑁 ) ) )
42 oveq2 ⊢ ( 𝑦 = 𝑛 → ( 1 ... 𝑦 ) = ( 1 ... 𝑛 ) )
43 42 iuneq1d ⊢ ( 𝑦 = 𝑛 → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
44 oveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 / 𝑁 ) = ( 𝑛 / 𝑁 ) )
45 44 oveq2d ⊢ ( 𝑦 = 𝑛 → ( 0 [,] ( 𝑦 / 𝑁 ) ) = ( 0 [,] ( 𝑛 / 𝑁 ) ) )
46 45 oveq2d ⊢ ( 𝑦 = 𝑛 → ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
47 46 oveq1d ⊢ ( 𝑦 = 𝑛 → ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) )
48 43 47 eleq12d ⊢ ( 𝑦 = 𝑛 → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ↔ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ) )
49 43 coeq2d ⊢ ( 𝑦 = 𝑛 → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) )
50 45 reseq2d ⊢ ( 𝑦 = 𝑛 → ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
51 49 50 eqeq12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ↔ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) )
52 48 51 anbi12d ⊢ ( 𝑦 = 𝑛 → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ↔ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) )
53 41 52 imbi12d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ↔ ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ) )
54 53 imbi2d ⊢ ( 𝑦 = 𝑛 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ) ) )
55 eleq1 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
56 oveq2 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 1 ... 𝑦 ) = ( 1 ... ( 𝑛 + 1 ) ) )
57 56 iuneq1d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) )
58 oveq1 ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝑦 / 𝑁 ) = ( ( 𝑛 + 1 ) / 𝑁 ) )
59 58 oveq2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 0 [,] ( 𝑦 / 𝑁 ) ) = ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
60 59 oveq2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
61 60 oveq1d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
62 57 61 eleq12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ↔ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ) )
63 57 coeq2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) )
64 59 reseq2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
65 63 64 eqeq12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ↔ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
66 62 65 anbi12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ↔ ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) )
67 55 66 imbi12d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ↔ ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) ) )
68 67 imbi2d ⊢ ( 𝑦 = ( 𝑛 + 1 ) → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ) ↔ ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) ) ) )
69 eleq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 ∈ ( 1 ... 𝑁 ) ↔ 𝑁 ∈ ( 1 ... 𝑁 ) ) )
70 oveq2 ⊢ ( 𝑦 = 𝑁 → ( 1 ... 𝑦 ) = ( 1 ... 𝑁 ) )
71 70 iuneq1d ⊢ ( 𝑦 = 𝑁 → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( 1 ... 𝑁 ) ( 𝑄 ‘ 𝑘 ) )
72 71 13 eqtr4di ⊢ ( 𝑦 = 𝑁 → ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) = 𝐾 )
73 oveq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 / 𝑁 ) = ( 𝑁 / 𝑁 ) )
74 73 oveq2d ⊢ ( 𝑦 = 𝑁 → ( 0 [,] ( 𝑦 / 𝑁 ) ) = ( 0 [,] ( 𝑁 / 𝑁 ) ) )
75 74 oveq2d ⊢ ( 𝑦 = 𝑁 → ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) )
76 75 oveq1d ⊢ ( 𝑦 = 𝑁 → ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) )
77 72 76 eleq12d ⊢ ( 𝑦 = 𝑁 → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ↔ 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ) )
78 72 coeq2d ⊢ ( 𝑦 = 𝑁 → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐹 ∘ 𝐾 ) )
79 74 reseq2d ⊢ ( 𝑦 = 𝑁 → ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) )
80 78 79 eqeq12d ⊢ ( 𝑦 = 𝑁 → ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ↔ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) )
81 77 80 anbi12d ⊢ ( 𝑦 = 𝑁 → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ↔ ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) ) )
82 69 81 imbi12d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ↔ ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) ) ) )
83 82 imbi2d ⊢ ( 𝑦 = 𝑁 → ( ( 𝜑 → ( 𝑦 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑦 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑦 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑦 / 𝑁 ) ) ) ) ) ) ↔ ( 𝜑 → ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) ) ) ) )
84 eluzfz1 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... 𝑁 ) )
85 16 84 syl ⊢ ( 𝜑 → 1 ∈ ( 1 ... 𝑁 ) )
86 eqid ⊢ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) = ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) )
87 1 2 3 4 5 6 7 8 9 10 11 12 86 cvmliftlem8 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) )
88 85 87 mpdan ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) )
89 1m1e0 ⊢ ( 1 − 1 ) = 0
90 89 oveq1i ⊢ ( ( 1 − 1 ) / 𝑁 ) = ( 0 / 𝑁 )
91 8 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
92 8 nnne0d ⊢ ( 𝜑 → 𝑁 ≠ 0 )
93 91 92 div0d ⊢ ( 𝜑 → ( 0 / 𝑁 ) = 0 )
94 90 93 eqtrid ⊢ ( 𝜑 → ( ( 1 − 1 ) / 𝑁 ) = 0 )
95 94 oveq1d ⊢ ( 𝜑 → ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) = ( 0 [,] ( 1 / 𝑁 ) ) )
96 95 oveq2d ⊢ ( 𝜑 → ( 𝐿 ↾t ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) )
97 96 oveq1d ⊢ ( 𝜑 → ( ( 𝐿 ↾t ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) )
98 88 97 eleqtrd ⊢ ( 𝜑 → ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) )
99 simpr ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → 1 ∈ ( 1 ... 𝑁 ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 86 cvmliftlem7 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 1 − 1 ) ) ‘ ( ( 1 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 1 − 1 ) / 𝑁 ) ) } ) )
101 1 2 3 4 5 6 7 8 9 10 11 12 86 99 100 cvmliftlem6 ⊢ ( ( 𝜑 ∧ 1 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 1 ) : ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) ) )
102 85 101 mpdan ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) : ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) ) )
103 102 simprd ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) )
104 95 reseq2d ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( ( 1 − 1 ) / 𝑁 ) [,] ( 1 / 𝑁 ) ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) )
105 103 104 eqtrd ⊢ ( 𝜑 → ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) )
106 98 105 jca ⊢ ( 𝜑 → ( ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) )
107 106 a1d ⊢ ( 𝜑 → ( 1 ∈ ( 1 ... 𝑁 ) → ( ( 𝑄 ‘ 1 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 1 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ( 𝑄 ‘ 1 ) ) = ( 𝐺 ↾ ( 0 [,] ( 1 / 𝑁 ) ) ) ) ) )
108 elnnuz ⊢ ( 𝑛 ∈ ℕ ↔ 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
109 108 biimpi ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
110 109 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
111 peano2fzr ⊢ ( ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
112 111 ex ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( 1 ... 𝑁 ) ) )
113 110 112 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → 𝑛 ∈ ( 1 ... 𝑁 ) ) )
114 113 imim1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ) )
115 eqid ⊢ ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
116 0re ⊢ 0 ∈ ℝ
117 14 simplbi ⊢ ( 𝜒 → ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) )
119 118 simprd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) )
120 elfznn ⊢ ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → ( 𝑛 + 1 ) ∈ ℕ )
121 119 120 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 + 1 ) ∈ ℕ )
122 121 nnred ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 + 1 ) ∈ ℝ )
123 8 adantr ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑁 ∈ ℕ )
124 122 123 nndivred ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ )
125 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ℝ )
126 116 124 125 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ℝ )
127 117 simpld ⊢ ( 𝜒 → 𝑛 ∈ ℕ )
128 127 adantl ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ℕ )
129 128 nnred ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ℝ )
130 129 123 nndivred ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ℝ )
131 icccld ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑛 / 𝑁 ) ∈ ℝ ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
132 116 130 131 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
133 11 fveq2i ⊢ ( Clsd ‘ 𝐿 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) )
134 132 133 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ 𝐿 ) )
135 ssun1 ⊢ ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
136 116 a1i ⊢ ( ( 𝜑 ∧ 𝜒 ) → 0 ∈ ℝ )
137 128 nnnn0d ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ℕ0 )
138 137 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝜒 ) → 0 ≤ 𝑛 )
139 123 nnred ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑁 ∈ ℝ )
140 123 nngt0d ⊢ ( ( 𝜑 ∧ 𝜒 ) → 0 < 𝑁 )
141 divge0 ⊢ ( ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → 0 ≤ ( 𝑛 / 𝑁 ) )
142 129 138 139 140 141 syl22anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → 0 ≤ ( 𝑛 / 𝑁 ) )
143 129 ltp1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 < ( 𝑛 + 1 ) )
144 ltdiv1 ⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑛 + 1 ) ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( 𝑛 < ( 𝑛 + 1 ) ↔ ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) ) )
145 129 122 139 140 144 syl112anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 < ( 𝑛 + 1 ) ↔ ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) ) )
146 143 145 mpbid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) < ( ( 𝑛 + 1 ) / 𝑁 ) )
147 130 124 146 ltled ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) )
148 elicc2 ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ ) → ( ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ↔ ( ( 𝑛 / 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑛 / 𝑁 ) ∧ ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
149 116 124 148 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ↔ ( ( 𝑛 / 𝑁 ) ∈ ℝ ∧ 0 ≤ ( 𝑛 / 𝑁 ) ∧ ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
150 130 142 147 149 mpbir3and ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
151 iccsplit ⊢ ( ( 0 ∈ ℝ ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ ∧ ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
152 136 124 150 151 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
153 135 152 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
154 uniretop ⊢ ℝ = ∪ ( topGen ‘ ran (,) )
155 11 unieqi ⊢ ∪ 𝐿 = ∪ ( topGen ‘ ran (,) )
156 154 155 eqtr4i ⊢ ℝ = ∪ 𝐿
157 156 restcldi ⊢ ( ( ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ℝ ∧ ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ 𝐿 ) ∧ ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
158 126 134 153 157 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ∈ ( Clsd ‘ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
159 icccld ⊢ ( ( ( 𝑛 / 𝑁 ) ∈ ℝ ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
160 130 124 159 syl2anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
161 160 133 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ 𝐿 ) )
162 ssun2 ⊢ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
163 162 152 sseqtrrid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
164 156 restcldi ⊢ ( ( ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ℝ ∧ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ 𝐿 ) ∧ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
165 126 161 163 164 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ ( Clsd ‘ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
166 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
167 11 166 eqeltri ⊢ 𝐿 ∈ Top
168 156 restuni ⊢ ( ( 𝐿 ∈ Top ∧ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ℝ ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
169 167 126 168 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
170 152 169 eqtr3d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
171 14 simprbi ⊢ ( 𝜒 → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) )
172 171 adantl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) )
173 172 simpld ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) )
174 eqid ⊢ ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) )
175 174 2 cnf ⊢ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ⟶ 𝐵 )
176 173 175 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ⟶ 𝐵 )
177 iccssre ⊢ ( ( 0 ∈ ℝ ∧ ( 𝑛 / 𝑁 ) ∈ ℝ ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ℝ )
178 116 130 177 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ℝ )
179 156 restuni ⊢ ( ( 𝐿 ∈ Top ∧ ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ℝ ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
180 167 178 179 sylancr ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( 𝑛 / 𝑁 ) ) = ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
181 180 feq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ( 0 [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ↔ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ∪ ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ⟶ 𝐵 ) )
182 176 181 mpbird ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ( 0 [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 )
183 eqid ⊢ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) )
184 simpr ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) )
185 1 2 3 4 5 6 7 8 9 10 11 12 183 cvmliftlem7 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) } ) )
186 1 2 3 4 5 6 7 8 9 10 11 12 183 184 185 cvmliftlem6 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
187 119 186 syldan ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
188 187 simpld ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 )
189 128 nncnd ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ℂ )
190 ax-1cn ⊢ 1 ∈ ℂ
191 pncan ⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
192 189 190 191 sylancl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
193 192 oveq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) = ( 𝑛 / 𝑁 ) )
194 193 oveq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
195 194 feq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ↔ ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ) )
196 188 195 mpbid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 )
197 176 ffund ⊢ ( ( 𝜑 ∧ 𝜒 ) → Fun ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
198 128 109 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ( ℤ≥ ‘ 1 ) )
199 eluzfz2 ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → 𝑛 ∈ ( 1 ... 𝑛 ) )
200 198 199 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ( 1 ... 𝑛 ) )
201 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ 𝑛 ) )
202 201 ssiun2s ⊢ ( 𝑛 ∈ ( 1 ... 𝑛 ) → ( 𝑄 ‘ 𝑛 ) ⊆ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
203 200 202 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ 𝑛 ) ⊆ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
204 peano2rem ⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
205 129 204 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 − 1 ) ∈ ℝ )
206 205 123 nndivred ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 − 1 ) / 𝑁 ) ∈ ℝ )
207 206 rexrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 − 1 ) / 𝑁 ) ∈ ℝ* )
208 130 rexrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ℝ* )
209 129 ltm1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 − 1 ) < 𝑛 )
210 ltdiv1 ⊢ ( ( ( 𝑛 − 1 ) ∈ ℝ ∧ 𝑛 ∈ ℝ ∧ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) ) → ( ( 𝑛 − 1 ) < 𝑛 ↔ ( ( 𝑛 − 1 ) / 𝑁 ) < ( 𝑛 / 𝑁 ) ) )
211 205 129 139 140 210 syl112anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 − 1 ) < 𝑛 ↔ ( ( 𝑛 − 1 ) / 𝑁 ) < ( 𝑛 / 𝑁 ) ) )
212 209 211 mpbid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 − 1 ) / 𝑁 ) < ( 𝑛 / 𝑁 ) )
213 206 130 212 ltled ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 − 1 ) / 𝑁 ) ≤ ( 𝑛 / 𝑁 ) )
214 ubicc2 ⊢ ( ( ( ( 𝑛 − 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑛 − 1 ) / 𝑁 ) ≤ ( 𝑛 / 𝑁 ) ) → ( 𝑛 / 𝑁 ) ∈ ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) )
215 207 208 213 214 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) )
216 198 119 111 syl2anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
217 eqid ⊢ ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) = ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) )
218 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → 𝑛 ∈ ( 1 ... 𝑁 ) )
219 1 2 3 4 5 6 7 8 9 10 11 12 217 cvmliftlem7 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑛 − 1 ) ) ‘ ( ( 𝑛 − 1 ) / 𝑁 ) ) ∈ ( ◡ 𝐹 “ { ( 𝐺 ‘ ( ( 𝑛 − 1 ) / 𝑁 ) ) } ) )
220 1 2 3 4 5 6 7 8 9 10 11 12 217 218 219 cvmliftlem6 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ 𝑛 ) : ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 𝑛 ) ) = ( 𝐺 ↾ ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) ) ) )
221 216 220 syldan ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ 𝑛 ) : ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝐹 ∘ ( 𝑄 ‘ 𝑛 ) ) = ( 𝐺 ↾ ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) ) ) )
222 221 simpld ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ 𝑛 ) : ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 )
223 222 fdmd ⊢ ( ( 𝜑 ∧ 𝜒 ) → dom ( 𝑄 ‘ 𝑛 ) = ( ( ( 𝑛 − 1 ) / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) )
224 215 223 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ dom ( 𝑄 ‘ 𝑛 ) )
225 funssfv ⊢ ( ( Fun ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∧ ( 𝑄 ‘ 𝑛 ) ⊆ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∧ ( 𝑛 / 𝑁 ) ∈ dom ( 𝑄 ‘ 𝑛 ) ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) = ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) )
226 197 203 224 225 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) = ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) )
227 192 fveq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑄 ‘ 𝑛 ) )
228 227 193 fveq12d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ 𝑛 ) ‘ ( 𝑛 / 𝑁 ) ) )
229 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem9 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) )
230 119 229 syldan ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) )
231 193 fveq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) )
232 230 231 eqtr3d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( ( 𝑛 + 1 ) − 1 ) ) ‘ ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) )
233 226 228 232 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) )
234 233 opeq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ⟨ ( 𝑛 / 𝑁 ) , ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ = ⟨ ( 𝑛 / 𝑁 ) , ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ )
235 234 sneqd ⊢ ( ( 𝜑 ∧ 𝜒 ) → { ⟨ ( 𝑛 / 𝑁 ) , ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } = { ⟨ ( 𝑛 / 𝑁 ) , ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } )
236 182 ffnd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) Fn ( 0 [,] ( 𝑛 / 𝑁 ) ) )
237 0xr ⊢ 0 ∈ ℝ*
238 237 a1i ⊢ ( ( 𝜑 ∧ 𝜒 ) → 0 ∈ ℝ* )
239 ubicc2 ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ 0 ≤ ( 𝑛 / 𝑁 ) ) → ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( 𝑛 / 𝑁 ) ) )
240 238 208 142 239 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( 𝑛 / 𝑁 ) ) )
241 fnressn ⊢ ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) Fn ( 0 [,] ( 𝑛 / 𝑁 ) ) ∧ ( 𝑛 / 𝑁 ) ∈ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ { ( 𝑛 / 𝑁 ) } ) = { ⟨ ( 𝑛 / 𝑁 ) , ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } )
242 236 240 241 syl2anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ { ( 𝑛 / 𝑁 ) } ) = { ⟨ ( 𝑛 / 𝑁 ) , ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } )
243 196 ffnd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) Fn ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
244 124 rexrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* )
245 lbicc2 ⊢ ( ( ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) ) → ( 𝑛 / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
246 208 244 147 245 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑛 / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) )
247 fnressn ⊢ ( ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) Fn ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∧ ( 𝑛 / 𝑁 ) ∈ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ { ( 𝑛 / 𝑁 ) } ) = { ⟨ ( 𝑛 / 𝑁 ) , ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } )
248 243 246 247 syl2anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ { ( 𝑛 / 𝑁 ) } ) = { ⟨ ( 𝑛 / 𝑁 ) , ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ‘ ( 𝑛 / 𝑁 ) ) ⟩ } )
249 235 242 248 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ { ( 𝑛 / 𝑁 ) } ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ { ( 𝑛 / 𝑁 ) } ) )
250 df-icc ⊢ [,] = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } )
251 xrmaxle ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( if ( 0 ≤ ( 𝑛 / 𝑁 ) , ( 𝑛 / 𝑁 ) , 0 ) ≤ 𝑧 ↔ ( 0 ≤ 𝑧 ∧ ( 𝑛 / 𝑁 ) ≤ 𝑧 ) ) )
252 xrlemin ⊢ ( ( 𝑧 ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* ) → ( 𝑧 ≤ if ( ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) , ( 𝑛 / 𝑁 ) , ( ( 𝑛 + 1 ) / 𝑁 ) ) ↔ ( 𝑧 ≤ ( 𝑛 / 𝑁 ) ∧ 𝑧 ≤ ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
253 250 251 252 ixxin ⊢ ( ( ( 0 ∈ ℝ* ∧ ( 𝑛 / 𝑁 ) ∈ ℝ* ) ∧ ( ( 𝑛 / 𝑁 ) ∈ ℝ* ∧ ( ( 𝑛 + 1 ) / 𝑁 ) ∈ ℝ* ) ) → ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( if ( 0 ≤ ( 𝑛 / 𝑁 ) , ( 𝑛 / 𝑁 ) , 0 ) [,] if ( ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) , ( 𝑛 / 𝑁 ) , ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
254 238 208 208 244 253 syl22anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( if ( 0 ≤ ( 𝑛 / 𝑁 ) , ( 𝑛 / 𝑁 ) , 0 ) [,] if ( ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) , ( 𝑛 / 𝑁 ) , ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
255 142 iftrued ⊢ ( ( 𝜑 ∧ 𝜒 ) → if ( 0 ≤ ( 𝑛 / 𝑁 ) , ( 𝑛 / 𝑁 ) , 0 ) = ( 𝑛 / 𝑁 ) )
256 147 iftrued ⊢ ( ( 𝜑 ∧ 𝜒 ) → if ( ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) , ( 𝑛 / 𝑁 ) , ( ( 𝑛 + 1 ) / 𝑁 ) ) = ( 𝑛 / 𝑁 ) )
257 255 256 oveq12d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( if ( 0 ≤ ( 𝑛 / 𝑁 ) , ( 𝑛 / 𝑁 ) , 0 ) [,] if ( ( 𝑛 / 𝑁 ) ≤ ( ( 𝑛 + 1 ) / 𝑁 ) , ( 𝑛 / 𝑁 ) , ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( ( 𝑛 / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) )
258 iccid ⊢ ( ( 𝑛 / 𝑁 ) ∈ ℝ* → ( ( 𝑛 / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) = { ( 𝑛 / 𝑁 ) } )
259 208 258 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑛 / 𝑁 ) [,] ( 𝑛 / 𝑁 ) ) = { ( 𝑛 / 𝑁 ) } )
260 254 257 259 3eqtrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = { ( 𝑛 / 𝑁 ) } )
261 260 reseq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ { ( 𝑛 / 𝑁 ) } ) )
262 260 reseq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ { ( 𝑛 / 𝑁 ) } ) )
263 249 261 262 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
264 fresaun ⊢ ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ( 0 [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 )
265 182 196 263 264 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 )
266 fzsuc ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ 1 ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
267 198 266 syl ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 1 ... ( 𝑛 + 1 ) ) = ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) )
268 267 iuneq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) = ∪ 𝑘 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ( 𝑄 ‘ 𝑘 ) )
269 iunxun ⊢ ∪ 𝑘 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ( 𝑄 ‘ 𝑘 ) = ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ∪ 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝑄 ‘ 𝑘 ) )
270 ovex ⊢ ( 𝑛 + 1 ) ∈ V
271 fveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
272 270 271 iunxsn ⊢ ∪ 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝑄 ‘ 𝑘 ) = ( 𝑄 ‘ ( 𝑛 + 1 ) )
273 272 uneq2i ⊢ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ∪ 𝑘 ∈ { ( 𝑛 + 1 ) } ( 𝑄 ‘ 𝑘 ) ) = ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
274 269 273 eqtri ⊢ ∪ 𝑘 ∈ ( ( 1 ... 𝑛 ) ∪ { ( 𝑛 + 1 ) } ) ( 𝑄 ‘ 𝑘 ) = ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
275 268 274 eqtr2di ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) )
276 275 feq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 ↔ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 ) )
277 265 276 mpbid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 )
278 170 feq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) : ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 ↔ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) : ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 ) )
279 277 278 mpbid ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) : ∪ ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ⟶ 𝐵 )
280 275 reseq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
281 fresaunres1 ⊢ ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ( 0 [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
282 182 196 263 281 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
283 280 282 eqtr3d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) )
284 167 a1i ⊢ ( ( 𝜑 ∧ 𝜒 ) → 𝐿 ∈ Top )
285 ovex ⊢ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ V
286 285 a1i ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ V )
287 restabs ⊢ ( ( 𝐿 ∈ Top ∧ ( 0 [,] ( 𝑛 / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∧ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ V ) → ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
288 284 153 286 287 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) = ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
289 288 oveq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) )
290 173 283 289 3eltr4d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ∈ ( ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) )
291 1 2 3 4 5 6 7 8 9 10 11 12 183 cvmliftlem8 ⊢ ( ( 𝜑 ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) ∈ ( ( 𝐿 ↾t ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
292 119 291 syldan ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) ∈ ( ( 𝐿 ↾t ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
293 194 oveq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐿 ↾t ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
294 293 oveq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝐿 ↾t ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
295 292 294 eleqtrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝑄 ‘ ( 𝑛 + 1 ) ) ∈ ( ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
296 275 reseq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
297 fresaunres2 ⊢ ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) : ( 0 [,] ( 𝑛 / 𝑁 ) ) ⟶ 𝐵 ∧ ( 𝑄 ‘ ( 𝑛 + 1 ) ) : ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⟶ 𝐵 ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝑄 ‘ ( 𝑛 + 1 ) ) ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∩ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
298 182 196 263 297 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
299 296 298 eqtr3d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝑄 ‘ ( 𝑛 + 1 ) ) )
300 restabs ⊢ ( ( 𝐿 ∈ Top ∧ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ⊆ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∧ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ∈ V ) → ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
301 284 163 286 300 syl3anc ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
302 301 oveq1d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) = ( ( 𝐿 ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
303 295 299 302 3eltr4d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ∈ ( ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ↾t ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
304 115 2 158 165 170 279 290 303 paste ⊢ ( ( 𝜑 ∧ 𝜒 ) → ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) )
305 152 reseq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
306 172 simprd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) )
307 187 simprd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
308 194 reseq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐺 ↾ ( ( ( ( 𝑛 + 1 ) − 1 ) / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) = ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
309 307 308 eqtrd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) = ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
310 306 309 uneq12d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) ∪ ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ∪ ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
311 coundi ⊢ ( 𝐹 ∘ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ) = ( ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) ∪ ( 𝐹 ∘ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) )
312 resundi ⊢ ( 𝐺 ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) = ( ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ∪ ( 𝐺 ↾ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
313 310 311 312 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 0 [,] ( 𝑛 / 𝑁 ) ) ∪ ( ( 𝑛 / 𝑁 ) [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
314 275 coeq2d ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∪ ( 𝑄 ‘ ( 𝑛 + 1 ) ) ) ) = ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) )
315 305 313 314 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) )
316 304 315 jca ⊢ ( ( 𝜑 ∧ 𝜒 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
317 14 316 sylan2br ⊢ ( ( 𝜑 ∧ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ∧ ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) )
318 317 expr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) ) ) → ( ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) )
319 114 318 animpimp2impd ⊢ ( 𝑛 ∈ ℕ → ( ( 𝜑 → ( 𝑛 ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑛 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... 𝑛 ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( 𝑛 / 𝑁 ) ) ) ) ) ) → ( 𝜑 → ( ( 𝑛 + 1 ) ∈ ( 1 ... 𝑁 ) → ( ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ∈ ( ( 𝐿 ↾t ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ ∪ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑄 ‘ 𝑘 ) ) = ( 𝐺 ↾ ( 0 [,] ( ( 𝑛 + 1 ) / 𝑁 ) ) ) ) ) ) ) )
320 40 54 68 83 107 319 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝜑 → ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) ) ) )
321 8 320 mpcom ⊢ ( 𝜑 → ( 𝑁 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) ) )
322 18 321 mpd ⊢ ( 𝜑 → ( 𝐾 ∈ ( ( 𝐿 ↾t ( 0 [,] ( 𝑁 / 𝑁 ) ) ) Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝐾 ) = ( 𝐺 ↾ ( 0 [,] ( 𝑁 / 𝑁 ) ) ) ) )