Metamath Proof Explorer

Theorem vdwlem9

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

Ref Expression
Hypotheses vdw.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem9.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem9.s ⊢ ( 𝜑 → ∀ 𝑠 ∈ Fin ∃ 𝑛 ∈ ℕ ∀ 𝑓 ∈ ( 𝑠 ↑m ( 1 ... 𝑛 ) ) 𝐾 MonoAP 𝑓 )
vdwlem9.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
vdwlem9.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem9.g ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
vdwlem9.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
vdwlem9.a ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↑m ( 1 ... 𝑉 ) ) 𝐾 MonoAP 𝑓 )
vdwlem9.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
vdwlem9.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
Assertion vdwlem9 ( 𝜑 → ( ⟨ ( 𝑀 + 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 vdwlem9.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
5 vdwlem9.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
6 vdwlem9.g ⊢ ( 𝜑 → ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
7 vdwlem9.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
8 vdwlem9.a ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↑m ( 1 ... 𝑉 ) ) 𝐾 MonoAP 𝑓 )
9 vdwlem9.h ⊢ ( 𝜑 → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
10 vdwlem9.f ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝑉 ) ↦ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) )
11 breq2 ⊢ ( 𝑓 = 𝐹 → ( 𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝐹 ) )
12 7 5 1 9 10 vdwlem4 ⊢ ( 𝜑 → 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
13 ovex ⊢ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ∈ V
14 ovex ⊢ ( 1 ... 𝑉 ) ∈ V
15 13 14 elmap ⊢ ( 𝐹 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↑m ( 1 ... 𝑉 ) ) ↔ 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
16 12 15 sylibr ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↑m ( 1 ... 𝑉 ) ) )
17 11 8 16 rspcdva ⊢ ( 𝜑 → 𝐾 MonoAP 𝐹 )
18 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
19 2 18 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
20 19 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
21 14 20 12 vdwmc ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 ↔ ∃ 𝑔 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) )
22 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
23 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) )
24 19 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐾 ∈ ℕ )
25 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ℕ )
26 simprlr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑑 ∈ ℕ )
27 vdwapid1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → 𝑎 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) )
28 24 25 26 27 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) )
29 23 28 sseldd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ( ◡ 𝐹 “ { 𝑔 } ) )
30 12 ffnd ⊢ ( 𝜑 → 𝐹 Fn ( 1 ... 𝑉 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐹 Fn ( 1 ... 𝑉 ) )
32 fniniseg ⊢ ( 𝐹 Fn ( 1 ... 𝑉 ) → ( 𝑎 ∈ ( ◡ 𝐹 “ { 𝑔 } ) ↔ ( 𝑎 ∈ ( 1 ... 𝑉 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑔 ) ) )
33 31 32 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 ∈ ( ◡ 𝐹 “ { 𝑔 } ) ↔ ( 𝑎 ∈ ( 1 ... 𝑉 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑔 ) ) )
34 29 33 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 ∈ ( 1 ... 𝑉 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑔 ) )
35 34 simprd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝐹 ‘ 𝑎 ) = 𝑔 )
36 12 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐹 : ( 1 ... 𝑉 ) ⟶ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
37 34 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ( 1 ... 𝑉 ) )
38 36 37 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
39 35 38 eqeltrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) )
40 rsp ⊢ ( ∀ 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) → ( 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
41 22 39 40 sylc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
42 7 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑉 ∈ ℕ )
43 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑊 ∈ ℕ )
44 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑅 ∈ Fin )
45 9 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐻 : ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) ⟶ 𝑅 )
46 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑀 ∈ ℕ )
47 ovex ⊢ ( 1 ... 𝑊 ) ∈ V
48 elmapg ⊢ ( ( 𝑅 ∈ Fin ∧ ( 1 ... 𝑊 ) ∈ V ) → ( 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↔ 𝑔 : ( 1 ... 𝑊 ) ⟶ 𝑅 ) )
49 44 47 48 sylancl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑔 ∈ ( 𝑅 ↑m ( 1 ... 𝑊 ) ) ↔ 𝑔 : ( 1 ... 𝑊 ) ⟶ 𝑅 ) )
50 39 49 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑔 : ( 1 ... 𝑊 ) ⟶ 𝑅 )
51 2 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
52 42 43 44 45 10 46 50 51 25 26 23 vdwlem7 ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
53 olc ⊢ ( ( 𝐾 + 1 ) MonoAP 𝑔 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
54 53 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝐾 + 1 ) MonoAP 𝑔 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
55 52 54 jaod ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) ) )
56 oveq1 ⊢ ( 𝑥 = 𝑎 → ( 𝑥 − 1 ) = ( 𝑎 − 1 ) )
57 56 oveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 − 1 ) + 𝑉 ) = ( ( 𝑎 − 1 ) + 𝑉 ) )
58 57 oveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) = ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) )
59 58 oveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) = ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) )
60 59 fveq2d ⊢ ( 𝑥 = 𝑎 → ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) = ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) )
61 60 mpteq2dv ⊢ ( 𝑥 = 𝑎 → ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑥 − 1 ) + 𝑉 ) ) ) ) ) = ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) )
62 47 mptex ⊢ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) ∈ V
63 61 10 62 fvmpt ⊢ ( 𝑎 ∈ ( 1 ... 𝑉 ) → ( 𝐹 ‘ 𝑎 ) = ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) )
64 37 63 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝐹 ‘ 𝑎 ) = ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) )
65 64 35 eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) = 𝑔 )
66 65 breq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝐾 + 1 ) MonoAP ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) ↔ ( 𝐾 + 1 ) MonoAP 𝑔 ) )
67 20 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝐾 ∈ ℕ0 )
68 peano2nn0 ⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
69 67 68 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝐾 + 1 ) ∈ ℕ0 )
70 nnm1nn0 ⊢ ( 𝑎 ∈ ℕ → ( 𝑎 − 1 ) ∈ ℕ0 )
71 25 70 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 − 1 ) ∈ ℕ0 )
72 nn0nnaddcl ⊢ ( ( ( 𝑎 − 1 ) ∈ ℕ0 ∧ 𝑉 ∈ ℕ ) → ( ( 𝑎 − 1 ) + 𝑉 ) ∈ ℕ )
73 71 42 72 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝑎 − 1 ) + 𝑉 ) ∈ ℕ )
74 43 73 nnmulcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ∈ ℕ )
75 25 42 nnaddcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 + 𝑉 ) ∈ ℕ )
76 43 75 nnmulcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 𝑎 + 𝑉 ) ) ∈ ℕ )
77 76 nnzd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 𝑎 + 𝑉 ) ) ∈ ℤ )
78 2nn ⊢ 2 ∈ ℕ
79 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑉 ∈ ℕ ) → ( 2 · 𝑉 ) ∈ ℕ )
80 78 7 79 sylancr ⊢ ( 𝜑 → ( 2 · 𝑉 ) ∈ ℕ )
81 5 80 nnmulcld ⊢ ( 𝜑 → ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ℕ )
82 81 nnzd ⊢ ( 𝜑 → ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ℤ )
83 82 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ℤ )
84 25 nnred ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ℝ )
85 42 nnred ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑉 ∈ ℝ )
86 elfzle2 ⊢ ( 𝑎 ∈ ( 1 ... 𝑉 ) → 𝑎 ≤ 𝑉 )
87 37 86 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ≤ 𝑉 )
88 84 85 85 87 leadd1dd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 + 𝑉 ) ≤ ( 𝑉 + 𝑉 ) )
89 42 nncnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑉 ∈ ℂ )
90 89 2timesd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 2 · 𝑉 ) = ( 𝑉 + 𝑉 ) )
91 88 90 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 + 𝑉 ) ≤ ( 2 · 𝑉 ) )
92 75 nnred ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 + 𝑉 ) ∈ ℝ )
93 80 nnred ⊢ ( 𝜑 → ( 2 · 𝑉 ) ∈ ℝ )
94 93 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 2 · 𝑉 ) ∈ ℝ )
95 43 nnred ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑊 ∈ ℝ )
96 43 nngt0d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 0 < 𝑊 )
97 lemul2 ⊢ ( ( ( 𝑎 + 𝑉 ) ∈ ℝ ∧ ( 2 · 𝑉 ) ∈ ℝ ∧ ( 𝑊 ∈ ℝ ∧ 0 < 𝑊 ) ) → ( ( 𝑎 + 𝑉 ) ≤ ( 2 · 𝑉 ) ↔ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ≤ ( 𝑊 · ( 2 · 𝑉 ) ) ) )
98 92 94 95 96 97 syl112anc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝑎 + 𝑉 ) ≤ ( 2 · 𝑉 ) ↔ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ≤ ( 𝑊 · ( 2 · 𝑉 ) ) ) )
99 91 98 mpbid ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 𝑎 + 𝑉 ) ) ≤ ( 𝑊 · ( 2 · 𝑉 ) ) )
100 eluz2 ⊢ ( ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ( ℤ≥ ‘ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ) ↔ ( ( 𝑊 · ( 𝑎 + 𝑉 ) ) ∈ ℤ ∧ ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ℤ ∧ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ≤ ( 𝑊 · ( 2 · 𝑉 ) ) ) )
101 77 83 99 100 syl3anbrc ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ( ℤ≥ ‘ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ) )
102 43 nncnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑊 ∈ ℂ )
103 1cnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 1 ∈ ℂ )
104 71 nn0cnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑎 − 1 ) ∈ ℂ )
105 104 89 addcld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝑎 − 1 ) + 𝑉 ) ∈ ℂ )
106 102 103 105 adddid ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 1 + ( ( 𝑎 − 1 ) + 𝑉 ) ) ) = ( ( 𝑊 · 1 ) + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) )
107 103 104 89 addassd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 1 + ( 𝑎 − 1 ) ) + 𝑉 ) = ( 1 + ( ( 𝑎 − 1 ) + 𝑉 ) ) )
108 ax-1cn ⊢ 1 ∈ ℂ
109 25 nncnd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → 𝑎 ∈ ℂ )
110 pncan3 ⊢ ( ( 1 ∈ ℂ ∧ 𝑎 ∈ ℂ ) → ( 1 + ( 𝑎 − 1 ) ) = 𝑎 )
111 108 109 110 sylancr ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 1 + ( 𝑎 − 1 ) ) = 𝑎 )
112 111 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 1 + ( 𝑎 − 1 ) ) + 𝑉 ) = ( 𝑎 + 𝑉 ) )
113 107 112 eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 1 + ( ( 𝑎 − 1 ) + 𝑉 ) ) = ( 𝑎 + 𝑉 ) )
114 113 oveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 1 + ( ( 𝑎 − 1 ) + 𝑉 ) ) ) = ( 𝑊 · ( 𝑎 + 𝑉 ) ) )
115 102 mulid1d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · 1 ) = 𝑊 )
116 115 oveq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝑊 · 1 ) + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) = ( 𝑊 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) )
117 106 114 116 3eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 𝑎 + 𝑉 ) ) = ( 𝑊 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) )
118 117 fveq2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ℤ≥ ‘ ( 𝑊 · ( 𝑎 + 𝑉 ) ) ) = ( ℤ≥ ‘ ( 𝑊 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) )
119 101 118 eleqtrd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( 𝑊 · ( 2 · 𝑉 ) ) ∈ ( ℤ≥ ‘ ( 𝑊 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) )
120 fvoveq1 ⊢ ( 𝑦 = 𝑧 → ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) = ( 𝐻 ‘ ( 𝑧 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) )
121 120 cbvmptv ⊢ ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) = ( 𝑧 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑧 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) )
122 44 69 43 74 45 119 121 vdwlem2 ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝐾 + 1 ) MonoAP ( 𝑦 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐻 ‘ ( 𝑦 + ( 𝑊 · ( ( 𝑎 − 1 ) + 𝑉 ) ) ) ) ) → ( 𝐾 + 1 ) MonoAP 𝐻 ) )
123 66 122 sylbird ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( 𝐾 + 1 ) MonoAP 𝑔 → ( 𝐾 + 1 ) MonoAP 𝐻 ) )
124 123 orim2d ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
125 55 124 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ( ⟨ 𝑀 , 𝐾 ⟩ PolyAP 𝑔 ∨ ( 𝐾 + 1 ) MonoAP 𝑔 ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
126 41 125 mpd ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ∧ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) ) ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) )
127 126 expr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ ) ) → ( ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
128 127 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
129 128 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑔 ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ℕ ( 𝑎 ( AP ‘ 𝐾 ) 𝑑 ) ⊆ ( ◡ 𝐹 “ { 𝑔 } ) → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
130 21 129 sylbid ⊢ ( 𝜑 → ( 𝐾 MonoAP 𝐹 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) ) )
131 17 130 mpd ⊢ ( 𝜑 → ( ⟨ ( 𝑀 + 1 ) , 𝐾 ⟩ PolyAP 𝐻 ∨ ( 𝐾 + 1 ) MonoAP 𝐻 ) )