Metamath Proof Explorer

Theorem vdwlem7

Description: Lemma for vdw . (Contributed by Mario Carneiro, 12-Sep-2014)

Ref Expression
Hypotheses vdwlem3.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
vdwlem3.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem4.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem4.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
vdwlem4.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
vdwlem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
vdwlem7.g ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
vdwlem7.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem7.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
vdwlem7.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
vdwlem7.s ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
Assertion vdwlem7 ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )

Proof

Step Hyp Ref Expression
1 vdwlem3.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
2 vdwlem3.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
3 vdwlem4.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
4 vdwlem4.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
5 vdwlem4.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
6 vdwlem7.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
7 vdwlem7.g ⊢ ( 𝜑 → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
8 vdwlem7.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
9 vdwlem7.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
10 vdwlem7.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
11 vdwlem7.s ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
12 ovex ⊢ ( 1 ... 𝑊 ) ∈ V
13 2nn0 ⊢ 2 ∈ ℕ0
14 eluznn0 ⊢ ( ( 2 ∈ ℕ0 ∧ 𝐾 ∈ ( ℤ≥ ‘ 2 ) ) → 𝐾 ∈ ℕ0 )
15 13 8 14 sylancr ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
16 eqid ⊢ ( 1 ... 𝑀 ) = ( 1 ... 𝑀 )
17 12 15 7 6 16 vdwpc ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) )
18 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑉 ∈ ℕ )
19 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑊 ∈ ℕ )
20 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑅 ∈ Fin )
21 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
22 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑀 ∈ ℕ )
23 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐺 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
24 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
25 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐴 ∈ ℕ )
26 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝐷 ∈ ℕ )
27 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐺 } ) )
28 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑎 ∈ ℕ )
29 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) )
30 nnex ⊢ ℕ ∈ V
31 ovex ⊢ ( 1 ... 𝑀 ) ∈ V
32 30 31 elmap ⊢ ( 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ↔ 𝑑 : ( 1 ... 𝑀 ) ⟶ ℕ )
33 29 32 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → 𝑑 : ( 1 ... 𝑀 ) ⟶ ℕ )
34 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) )
35 fveq2 ⊢ ( 𝑖 = 𝑘 → ( 𝑑 ‘ 𝑖 ) = ( 𝑑 ‘ 𝑘 ) )
36 35 oveq2d ⊢ ( 𝑖 = 𝑘 → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) = ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) )
37 36 35 oveq12d ⊢ ( 𝑖 = 𝑘 → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) = ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) )
38 36 fveq2d ⊢ ( 𝑖 = 𝑘 → ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) = ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) )
39 38 sneqd ⊢ ( 𝑖 = 𝑘 → { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } = { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } )
40 39 imaeq2d ⊢ ( 𝑖 = 𝑘 → ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
41 37 40 sseq12d ⊢ ( 𝑖 = 𝑘 → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) ) )
42 41 cbvralvw ⊢ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
43 34 42 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ∀ 𝑘 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑘 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) } ) )
44 38 cbvmptv ⊢ ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑘 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑘 ) ) ) )
45 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 )
46 eqid ⊢ ( 𝑎 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) ) = ( 𝑎 + ( 𝑊 · ( ( 𝐴 + ( 𝑉 − 𝐷 ) ) − 1 ) ) )
47 eqid ⊢ ( 𝑗 ∈ ( 1 ... ( 𝑀 + 1 ) ) ↦ ( if ( 𝑗 = ( 𝑀 + 1 ) , 0 , ( 𝑑 ‘ 𝑗 ) ) + ( 𝑊 · 𝐷 ) ) ) = ( 𝑗 ∈ ( 1 ... ( 𝑀 + 1 ) ) ↦ ( if ( 𝑗 = ( 𝑀 + 1 ) , 0 , ( 𝑑 ‘ 𝑗 ) ) + ( 𝑊 · 𝐷 ) ) )
48 18 19 20 21 5 22 23 24 25 26 27 28 33 43 44 45 46 47 vdwlem6 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) )
49 48 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )
50 49 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 𝑀 ) ) ( ∀ 𝑖 ∈ ( 1 ... 𝑀 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐺 “ { ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 𝑀 ) ↦ ( 𝐺 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 𝑀 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )
51 17 50 sylbid ⊢ ( 𝜑 → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝐺 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐺 ) ) )