Metamath Proof Explorer

Theorem vdwlem10

Description: Lemma for vdw . Set up secondary induction on M . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem9.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem9.s ⊢ ( 𝜑 → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
vdwlem10.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
Assertion vdwlem10 ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )

Proof

Step Hyp Ref Expression
1 vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem9.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3 vdwlem9.s ⊢ ( 𝜑 → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
4 vdwlem10.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 opeq1 ⊢ ( 𝑥 = 1 → ⟨ 𝑥 , 𝐾 ⟩ = ⟨ 1 , 𝐾 ⟩ )
6 5 breq1d ⊢ ( 𝑥 = 1 → ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ) )
7 6 orbi1d ⊢ ( 𝑥 = 1 → ( ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
8 7 rexralbidv ⊢ ( 𝑥 = 1 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
9 8 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
10 opeq1 ⊢ ( 𝑥 = 𝑚 → ⟨ 𝑥 , 𝐾 ⟩ = ⟨ 𝑚 , 𝐾 ⟩ )
11 10 breq1d ⊢ ( 𝑥 = 𝑚 → ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ) )
12 11 orbi1d ⊢ ( 𝑥 = 𝑚 → ( ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
13 12 rexralbidv ⊢ ( 𝑥 = 𝑚 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
14 13 imbi2d ⊢ ( 𝑥 = 𝑚 → ( ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
15 opeq1 ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ⟨ 𝑥 , 𝐾 ⟩ = ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ )
16 15 breq1d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ) )
17 16 orbi1d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
18 17 rexralbidv ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
19 18 imbi2d ⊢ ( 𝑥 = ( 𝑚 + 1 ) → ( ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
20 opeq1 ⊢ ( 𝑥 = 𝑀 → ⟨ 𝑥 , 𝐾 ⟩ = ⟨ 𝑀 , 𝐾 ⟩ )
21 20 breq1d ⊢ ( 𝑥 = 𝑀 → ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ) )
22 21 orbi1d ⊢ ( 𝑥 = 𝑀 → ( ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
23 22 rexralbidv ⊢ ( 𝑥 = 𝑀 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
24 23 imbi2d ⊢ ( 𝑥 = 𝑀 → ( ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑥 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ↔ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
25 oveq1 ⊢ ( 𝑠 = 𝑅 → ( 𝑠 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... 𝑛 ) ) )
26 25 raleqdv ⊢ ( 𝑠 = 𝑅 → ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
27 26 rexbidv ⊢ ( 𝑠 = 𝑅 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ) )
28 27 3 1 rspcdva ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
29 oveq2 ⊢ ( 𝑛 = 𝑤 → ( 1 ... 𝑛 ) = ( 1 ... 𝑤 ) )
30 29 oveq2d ⊢ ( 𝑛 = 𝑤 → ( 𝑅 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... 𝑤 ) ) )
31 30 raleqdv ⊢ ( 𝑛 = 𝑤 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 ) )
32 31 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑤 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 )
33 28 32 sylib ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 )
34 breq2 ⊢ ( 𝑓 = 𝑔 → ( 𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝑔 ) )
35 34 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 )
36 2nn ⊢ 2 ∈ ℕ
37 simpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → 𝑤 ∈ ℕ )
38 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( 2 · 𝑤 ) ∈ ℕ )
39 36 37 38 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( 2 · 𝑤 ) ∈ ℕ )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → 𝑅 ∈ Fin )
41 ovex ⊢ ( 1 ... ( 2 · 𝑤 ) ) ∈ V
42 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... ( 2 · 𝑤 ) ) ∈ V ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ↔ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) )
43 40 41 42 sylancl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ↔ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) )
44 43 biimpa ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ) → 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 )
45 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 )
46 elfznn ⊢ ( 𝑦 ∈ ( 1 ... 𝑤 ) → 𝑦 ∈ ℕ )
47 46 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑦 ∈ ℕ )
48 47 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑦 ∈ ℝ )
49 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑤 ∈ ℕ )
50 49 nnred ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑤 ∈ ℝ )
51 elfzle2 ⊢ ( 𝑦 ∈ ( 1 ... 𝑤 ) → 𝑦 ≤ 𝑤 )
52 51 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑦 ≤ 𝑤 )
53 48 50 50 52 leadd1dd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑦 + 𝑤 ) ≤ ( 𝑤 + 𝑤 ) )
54 49 nncnd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → 𝑤 ∈ ℂ )
55 54 2timesd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 2 · 𝑤 ) = ( 𝑤 + 𝑤 ) )
56 53 55 breqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑦 + 𝑤 ) ≤ ( 2 · 𝑤 ) )
57 47 49 nnaddcld ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑦 + 𝑤 ) ∈ ℕ )
58 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
59 57 58 eleqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑦 + 𝑤 ) ∈ ( ℤ≥ ‘ 1 ) )
60 39 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 2 · 𝑤 ) ∈ ℕ )
61 60 nnzd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 2 · 𝑤 ) ∈ ℤ )
62 elfz5 ⊢ ( ( ( 𝑦 + 𝑤 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 · 𝑤 ) ∈ ℤ ) → ( ( 𝑦 + 𝑤 ) ∈ ( 1 ... ( 2 · 𝑤 ) ) ↔ ( 𝑦 + 𝑤 ) ≤ ( 2 · 𝑤 ) ) )
63 59 61 62 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( ( 𝑦 + 𝑤 ) ∈ ( 1 ... ( 2 · 𝑤 ) ) ↔ ( 𝑦 + 𝑤 ) ≤ ( 2 · 𝑤 ) ) )
64 56 63 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑦 + 𝑤 ) ∈ ( 1 ... ( 2 · 𝑤 ) ) )
65 45 64 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ 𝑦 ∈ ( 1 ... 𝑤 ) ) → ( 𝑓 ‘ ( 𝑦 + 𝑤 ) ) ∈ 𝑅 )
66 fvoveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) = ( 𝑓 ‘ ( 𝑦 + 𝑤 ) ) )
67 66 cbvmptv ⊢ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) = ( 𝑦 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑦 + 𝑤 ) ) )
68 65 67 fmptd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) : ( 1 ... 𝑤 ) ⟶ 𝑅 )
69 ovex ⊢ ( 1 ... 𝑤 ) ∈ V
70 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑤 ) ∈ V ) → ( ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↔ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) : ( 1 ... 𝑤 ) ⟶ 𝑅 ) )
71 40 69 70 sylancl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↔ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) : ( 1 ... 𝑤 ) ⟶ 𝑅 ) )
72 71 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) : ( 1 ... 𝑤 ) ⟶ 𝑅 ) → ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) )
73 68 72 syldan ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) )
74 breq2 ⊢ ( 𝑔 = ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) → ( 𝐾 MonoAP 𝑔 ↔ 𝐾 MonoAP ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ) )
75 74 rspcv ⊢ ( ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → 𝐾 MonoAP ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ) )
76 73 75 syl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → 𝐾 MonoAP ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ) )
77 2nn0 ⊢ 2 ∈ ℕ0
78 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
79 eluznn0 ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℕ0 )
80 77 78 79 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → 𝐾 ∈ ℕ0 )
81 69 80 68 vdwmc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( 𝐾 MonoAP ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) ↔ ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) )
82 40 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝑅 ∈ Fin )
83 78 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
84 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝑤 ∈ ℕ )
85 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 )
86 vex ⊢ 𝑐 ∈ V
87 simprll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝑎 ∈ ℕ )
88 simprlr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → 𝑑 ∈ ℕ )
89 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) )
90 82 83 84 85 86 87 88 89 67 vdwlem8 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 )
91 90 orcd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) ) ) → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
92 91 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
93 92 rexlimdvva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
94 93 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( ∃ 𝑐 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) “ { 𝑐 } ) → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
95 81 94 sylbid ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( 𝐾 MonoAP ( 𝑥 ∈ ( 1 ... 𝑤 ) ↦ ( 𝑓 ‘ ( 𝑥 + 𝑤 ) ) ) → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
96 76 95 syld ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 : ( 1 ... ( 2 · 𝑤 ) ) ⟶ 𝑅 ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
97 44 96 syldan ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) ∧ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
98 97 ralrimdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
99 oveq2 ⊢ ( 𝑛 = ( 2 · 𝑤 ) → ( 1 ... 𝑛 ) = ( 1 ... ( 2 · 𝑤 ) ) )
100 99 oveq2d ⊢ ( 𝑛 = ( 2 · 𝑤 ) → ( 𝑅 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) )
101 100 raleqdv ⊢ ( 𝑛 = ( 2 · 𝑤 ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
102 101 rspcev ⊢ ( ( ( 2 · 𝑤 ) ∈ ℕ ∧ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 2 · 𝑤 ) ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
103 39 98 102 syl6an ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑔 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
104 35 103 biimtrid ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℕ ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
105 104 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) 𝐾 MonoAP 𝑓 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
106 33 105 mpd ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
107 breq2 ⊢ ( 𝑓 = 𝑔 → ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ) )
108 breq2 ⊢ ( 𝑓 = 𝑔 → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
109 107 108 orbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
110 109 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
111 30 raleqdv ⊢ ( 𝑛 = 𝑤 → ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ↔ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
112 110 111 bitrid ⊢ ( 𝑛 = 𝑤 → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
113 112 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∃ 𝑤 ∈ ℕ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
114 oveq2 ⊢ ( 𝑛 = 𝑣 → ( 1 ... 𝑛 ) = ( 1 ... 𝑣 ) )
115 114 oveq2d ⊢ ( 𝑛 = 𝑣 → ( 𝑠 ↑m ( 1 ... 𝑛 ) ) = ( 𝑠 ↑m ( 1 ... 𝑣 ) ) )
116 115 raleqdv ⊢ ( 𝑛 = 𝑣 → ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) )
117 116 cbvrexvw ⊢ ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑣 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 )
118 oveq1 ⊢ ( 𝑠 = ( 𝑅 ↑m ( 1 ... 𝑤 ) ) → ( 𝑠 ↑m ( 1 ... 𝑣 ) ) = ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) )
119 118 raleqdv ⊢ ( 𝑠 = ( 𝑅 ↑m ( 1 ... 𝑤 ) ) → ( ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ↔ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) )
120 119 rexbidv ⊢ ( 𝑠 = ( 𝑅 ↑m ( 1 ... 𝑤 ) ) → ( ∃ 𝑣 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑣 ∈ ℕ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) )
121 117 120 bitrid ⊢ ( 𝑠 = ( 𝑅 ↑m ( 1 ... 𝑤 ) ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 ↔ ∃ 𝑣 ∈ ℕ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) )
122 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
123 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) → 𝑅 ∈ Fin )
124 fzfi ⊢ ( 1 ... 𝑤 ) ∈ Fin
125 mapfi ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑤 ) ∈ Fin ) → ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ∈ Fin )
126 123 124 125 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) → ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ∈ Fin )
127 121 122 126 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) → ∃ 𝑣 ∈ ℕ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 )
128 simprll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → 𝑤 ∈ ℕ )
129 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → 𝑣 ∈ ℕ )
130 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑣 ∈ ℕ ) → ( 2 · 𝑣 ) ∈ ℕ )
131 36 130 mpan ⊢ ( 𝑣 ∈ ℕ → ( 2 · 𝑣 ) ∈ ℕ )
132 nnmulcl ⊢ ( ( 𝑤 ∈ ℕ ∧ ( 2 · 𝑣 ) ∈ ℕ ) → ( 𝑤 · ( 2 · 𝑣 ) ) ∈ ℕ )
133 131 132 sylan2 ⊢ ( ( 𝑤 ∈ ℕ ∧ 𝑣 ∈ ℕ ) → ( 𝑤 · ( 2 · 𝑣 ) ) ∈ ℕ )
134 128 129 133 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → ( 𝑤 · ( 2 · 𝑣 ) ) ∈ ℕ )
135 simp1l ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝜑 )
136 135 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝑅 ∈ Fin )
137 135 2 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
138 135 3 syl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
139 simp1r ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝑚 ∈ ℕ )
140 simp2ll ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝑤 ∈ ℕ )
141 simp2lr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
142 breq2 ⊢ ( 𝑔 = 𝑘 → ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ↔ ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑘 ) )
143 breq2 ⊢ ( 𝑔 = 𝑘 → ( ( 𝐾 + 1 ) MonoAP 𝑔 ↔ ( 𝐾 + 1 ) MonoAP 𝑘 ) )
144 142 143 orbi12d ⊢ ( 𝑔 = 𝑘 → ( ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ↔ ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑘 ∨ ( 𝐾 + 1 ) MonoAP 𝑘 ) ) )
145 144 cbvralvw ⊢ ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ↔ ∀ 𝑘 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑘 ∨ ( 𝐾 + 1 ) MonoAP 𝑘 ) )
146 141 145 sylib ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ∀ 𝑘 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑘 ∨ ( 𝐾 + 1 ) MonoAP 𝑘 ) )
147 simp2rl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → 𝑣 ∈ ℕ )
148 simp2rr ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 )
149 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) )
150 ovex ⊢ ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ∈ V
151 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ∈ V ) → ( ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ↔ ℎ : ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ⟶ 𝑅 ) )
152 136 150 151 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ( ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ↔ ℎ : ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ⟶ 𝑅 ) )
153 149 152 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ℎ : ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ⟶ 𝑅 )
154 fvoveq1 ⊢ ( 𝑦 = 𝑢 → ( ℎ ‘ ( 𝑦 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) = ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) )
155 154 cbvmptv ⊢ ( 𝑦 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑦 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) ) = ( 𝑢 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) )
156 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 − 1 ) = ( 𝑧 − 1 ) )
157 156 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 − 1 ) + 𝑣 ) = ( ( 𝑧 − 1 ) + 𝑣 ) )
158 157 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) = ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) )
159 158 oveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑢 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) = ( 𝑢 + ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) ) )
160 159 fveq2d ⊢ ( 𝑥 = 𝑧 → ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) = ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) ) ) )
161 160 mpteq2dv ⊢ ( 𝑥 = 𝑧 → ( 𝑢 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) ) = ( 𝑢 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) ) ) ) )
162 155 161 eqtrid ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑦 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) ) = ( 𝑢 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) ) ) ) )
163 162 cbvmptv ⊢ ( 𝑥 ∈ ( 1 ... 𝑣 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑦 + ( 𝑤 · ( ( 𝑥 − 1 ) + 𝑣 ) ) ) ) ) ) = ( 𝑧 ∈ ( 1 ... 𝑣 ) ↦ ( 𝑢 ∈ ( 1 ... 𝑤 ) ↦ ( ℎ ‘ ( 𝑢 + ( 𝑤 · ( ( 𝑧 − 1 ) + 𝑣 ) ) ) ) ) )
164 136 137 138 139 140 146 147 148 153 163 vdwlem9 ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ∧ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ) → ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) )
165 164 3expia ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → ( ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) → ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) ) )
166 165 ralrimiv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → ∀ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) )
167 oveq2 ⊢ ( 𝑛 = ( 𝑤 · ( 2 · 𝑣 ) ) → ( 1 ... 𝑛 ) = ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) )
168 167 oveq2d ⊢ ( 𝑛 = ( 𝑤 · ( 2 · 𝑣 ) ) → ( 𝑅 ↑m ( 1 ... 𝑛 ) ) = ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) )
169 168 raleqdv ⊢ ( 𝑛 = ( 𝑤 · ( 2 · 𝑣 ) ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
170 breq2 ⊢ ( 𝑓 = ℎ → ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ↔ ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ) )
171 breq2 ⊢ ( 𝑓 = ℎ → ( ( 𝐾 + 1 ) MonoAP 𝑓 ↔ ( 𝐾 + 1 ) MonoAP ℎ ) )
172 170 171 orbi12d ⊢ ( 𝑓 = ℎ → ( ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) ) )
173 172 cbvralvw ⊢ ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) )
174 169 173 bitrdi ⊢ ( 𝑛 = ( 𝑤 · ( 2 · 𝑣 ) ) → ( ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ↔ ∀ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) ) )
175 174 rspcev ⊢ ( ( ( 𝑤 · ( 2 · 𝑣 ) ) ∈ ℕ ∧ ∀ ℎ ∈ ( 𝑅 ↑m ( 1 ... ( 𝑤 · ( 2 · 𝑣 ) ) ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP ℎ ∨ ( 𝐾 + 1 ) MonoAP ℎ ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
176 134 166 175 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
177 176 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) ∧ ( 𝑣 ∈ ℕ ∧ ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ↑m ( 1 ... 𝑣 ) ) 𝐾 MonoAP 𝑓 ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
178 127 177 rexlimddv ⊢ ( ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) ∧ ( 𝑤 ∈ ℕ ∧ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )
179 178 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑤 ∈ ℕ ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑤 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
180 113 179 biimtrid ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
181 180 expcom ⊢ ( 𝑚 ∈ ℕ → ( 𝜑 → ( ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
182 181 a2d ⊢ ( 𝑚 ∈ ℕ → ( ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑚 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) → ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ ( 𝑚 + 1 ) , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) ) )
183 9 14 19 24 106 182 nnind ⊢ ( 𝑀 ∈ ℕ → ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) ) )
184 4 183 mpcom ⊢ ( 𝜑 → ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑅 ↑m ( 1 ... 𝑛 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑓 ∨ ( 𝐾 + 1 ) MonoAP 𝑓 ) )