Metamath Proof Explorer

Theorem cvmliftlem5

Description: Lemma for cvmlift . Definition of Q at a successor. This is a function defined on W as ` ``' ( T |`I ) o. G where I is the unique covering set of 2nd( TM ) that contains Q ( M - 1 ) evaluated at the last defined point, namely ( M - 1 ) / N (note that for M = 1 this is using the seed value Q ( 0 ) ( 0 ) = P ). (Contributed by Mario Carneiro, 15-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 cvmliftlem5 ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 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 0z ⊢ 0 ∈ ℤ
15 simpr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℕ )
16 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
17 1e0p1 ⊢ 1 = ( 0 + 1 )
18 17 fveq2i ⊢ ( ℤ≥ ‘ 1 ) = ( ℤ≥ ‘ ( 0 + 1 ) )
19 16 18 eqtri ⊢ ℕ = ( ℤ≥ ‘ ( 0 + 1 ) )
20 15 19 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) )
21 seqm1 ⊢ ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ( ℤ≥ ‘ ( 0 + 1 ) ) ) → ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ 𝑀 ) = ( ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) ) )
22 14 20 21 sylancr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ 𝑀 ) = ( ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) ) )
23 12 fveq1i ⊢ ( 𝑄 ‘ 𝑀 ) = ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ 𝑀 )
24 12 fveq1i ⊢ ( 𝑄 ‘ ( 𝑀 − 1 ) ) = ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ ( 𝑀 − 1 ) )
25 24 oveq1i ⊢ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) ) = ( ( seq 0 ( ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) , ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ) ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) )
26 22 23 25 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) ) )
27 0nnn ⊢ ¬ 0 ∈ ℕ
28 disjsn ⊢ ( ( ℕ ∩ { 0 } ) = ∅ ↔ ¬ 0 ∈ ℕ )
29 27 28 mpbir ⊢ ( ℕ ∩ { 0 } ) = ∅
30 fnresi ⊢ ( I ↾ ℕ ) Fn ℕ
31 c0ex ⊢ 0 ∈ V
32 snex ⊢ { ⟨ 0 , 𝑃 ⟩ } ∈ V
33 31 32 fnsn ⊢ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } Fn { 0 }
34 fvun1 ⊢ ( ( ( I ↾ ℕ ) Fn ℕ ∧ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } Fn { 0 } ∧ ( ( ℕ ∩ { 0 } ) = ∅ ∧ 𝑀 ∈ ℕ ) ) → ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) = ( ( I ↾ ℕ ) ‘ 𝑀 ) )
35 30 33 34 mp3an12 ⊢ ( ( ( ℕ ∩ { 0 } ) = ∅ ∧ 𝑀 ∈ ℕ ) → ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) = ( ( I ↾ ℕ ) ‘ 𝑀 ) )
36 29 15 35 sylancr ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) = ( ( I ↾ ℕ ) ‘ 𝑀 ) )
37 fvresi ⊢ ( 𝑀 ∈ ℕ → ( ( I ↾ ℕ ) ‘ 𝑀 ) = 𝑀 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( ( I ↾ ℕ ) ‘ 𝑀 ) = 𝑀 )
39 36 38 eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) = 𝑀 )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) ( ( ( I ↾ ℕ ) ∪ { ⟨ 0 , { ⟨ 0 , 𝑃 ⟩ } ⟩ } ) ‘ 𝑀 ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) 𝑀 ) )
41 fvexd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∈ V )
42 simpr ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
43 42 oveq1d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑚 − 1 ) = ( 𝑀 − 1 ) )
44 43 oveq1d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 − 1 ) / 𝑁 ) = ( ( 𝑀 − 1 ) / 𝑁 ) )
45 42 oveq1d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑚 / 𝑁 ) = ( 𝑀 / 𝑁 ) )
46 44 45 oveq12d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) = ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) )
47 46 13 eqtr4di ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) = 𝑊 )
48 42 fveq2d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑇 ‘ 𝑚 ) = ( 𝑇 ‘ 𝑀 ) )
49 48 fveq2d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) )
50 simpl ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) )
51 50 44 fveq12d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) = ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) )
52 51 eleq1d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ↔ ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
53 49 52 riotaeqbidv ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) = ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) )
54 53 reseq2d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) = ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
55 54 cnveqd ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) = ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) )
56 55 fveq1d ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) = ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) )
57 47 56 mpteq12dv ⊢ ( ( 𝑥 = ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∧ 𝑚 = 𝑀 ) → ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
58 eqid ⊢ ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) = ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
59 ovex ⊢ ( ( ( 𝑀 − 1 ) / 𝑁 ) [,] ( 𝑀 / 𝑁 ) ) ∈ V
60 13 59 eqeltri ⊢ 𝑊 ∈ V
61 60 mptex ⊢ ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ∈ V
62 57 58 61 ovmpoa ⊢ ( ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ∈ V ∧ 𝑀 ∈ ℕ ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
63 41 62 sylan ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ( 𝑥 ∈ V , 𝑚 ∈ ℕ ↦ ( 𝑧 ∈ ( ( ( 𝑚 − 1 ) / 𝑁 ) [,] ( 𝑚 / 𝑁 ) ) ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑚 ) ) ( 𝑥 ‘ ( ( 𝑚 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) ) 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )
64 26 40 63 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑀 ∈ ℕ ) → ( 𝑄 ‘ 𝑀 ) = ( 𝑧 ∈ 𝑊 ↦ ( ◡ ( 𝐹 ↾ ( ℩ 𝑏 ∈ ( 2nd ‘ ( 𝑇 ‘ 𝑀 ) ) ( ( 𝑄 ‘ ( 𝑀 − 1 ) ) ‘ ( ( 𝑀 − 1 ) / 𝑁 ) ) ∈ 𝑏 ) ) ‘ ( 𝐺 ‘ 𝑧 ) ) ) )