Metamath Proof Explorer

Theorem vdwlem8

Description: Lemma for vdw . (Contributed by Mario Carneiro, 18-Aug-2014)

Ref Expression
Hypotheses vdwlem8.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
vdwlem8.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
vdwlem8.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem8.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 2 · 𝑊 ) ) ⟶ 𝑅 )
vdwlem8.c ⊢ 𝐶 ∈ V
vdwlem8.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
vdwlem8.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
vdwlem8.s ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐺 “ { 𝐶 } ) )
vdwlem8.g ⊢ 𝐺 = ( 𝑥 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 + 𝑊 ) ) )
Assertion vdwlem8 ( 𝜑 → ⟨ 1 , 𝐾 ⟩ PolyAP 𝐹 )

Proof

Step Hyp Ref Expression
1 vdwlem8.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
2 vdwlem8.k ⊢ ( 𝜑 → 𝐾 ∈ ( ℤ≥ ‘ 2 ) )
3 vdwlem8.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
4 vdwlem8.f ⊢ ( 𝜑 → 𝐹 : ( 1 ... ( 2 · 𝑊 ) ) ⟶ 𝑅 )
5 vdwlem8.c ⊢ 𝐶 ∈ V
6 vdwlem8.a ⊢ ( 𝜑 → 𝐴 ∈ ℕ )
7 vdwlem8.d ⊢ ( 𝜑 → 𝐷 ∈ ℕ )
8 vdwlem8.s ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐺 “ { 𝐶 } ) )
9 vdwlem8.g ⊢ 𝐺 = ( 𝑥 ∈ ( 1 ... 𝑊 ) ↦ ( 𝐹 ‘ ( 𝑥 + 𝑊 ) ) )
10 6 nncnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
11 7 nncnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
12 10 11 addcomd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) = ( 𝐷 + 𝐴 ) )
13 12 oveq2d ⊢ ( 𝜑 → ( 𝑊 − ( 𝐴 + 𝐷 ) ) = ( 𝑊 − ( 𝐷 + 𝐴 ) ) )
14 3 nncnd ⊢ ( 𝜑 → 𝑊 ∈ ℂ )
15 14 11 10 subsub4d ⊢ ( 𝜑 → ( ( 𝑊 − 𝐷 ) − 𝐴 ) = ( 𝑊 − ( 𝐷 + 𝐴 ) ) )
16 13 15 eqtr4d ⊢ ( 𝜑 → ( 𝑊 − ( 𝐴 + 𝐷 ) ) = ( ( 𝑊 − 𝐷 ) − 𝐴 ) )
17 16 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 + 𝐴 ) + ( 𝑊 − ( 𝐴 + 𝐷 ) ) ) = ( ( 𝐴 + 𝐴 ) + ( ( 𝑊 − 𝐷 ) − 𝐴 ) ) )
18 14 11 subcld ⊢ ( 𝜑 → ( 𝑊 − 𝐷 ) ∈ ℂ )
19 10 10 18 ppncand ⊢ ( 𝜑 → ( ( 𝐴 + 𝐴 ) + ( ( 𝑊 − 𝐷 ) − 𝐴 ) ) = ( 𝐴 + ( 𝑊 − 𝐷 ) ) )
20 17 19 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + 𝐴 ) + ( 𝑊 − ( 𝐴 + 𝐷 ) ) ) = ( 𝐴 + ( 𝑊 − 𝐷 ) ) )
21 6 6 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝐴 ) ∈ ℕ )
22 cnvimass ⊢ ( ◡ 𝐺 “ { 𝐶 } ) ⊆ dom 𝐺
23 fvex ⊢ ( 𝐹 ‘ ( 𝑥 + 𝑊 ) ) ∈ V
24 23 9 dmmpti ⊢ dom 𝐺 = ( 1 ... 𝑊 )
25 22 24 sseqtri ⊢ ( ◡ 𝐺 “ { 𝐶 } ) ⊆ ( 1 ... 𝑊 )
26 8 25 sstrdi ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( 1 ... 𝑊 ) )
27 ssun2 ⊢ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ⊆ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
28 uz2m1nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → ( 𝐾 − 1 ) ∈ ℕ )
29 2 28 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ )
30 6 7 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ℕ )
31 vdwapid1 ⊢ ( ( ( 𝐾 − 1 ) ∈ ℕ ∧ ( 𝐴 + 𝐷 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 + 𝐷 ) ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
32 29 30 7 31 syl3anc ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) )
33 27 32 sselid ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
34 eluz2nn ⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 2 ) → 𝐾 ∈ ℕ )
35 2 34 syl ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
36 35 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
37 ax-1cn ⊢ 1 ∈ ℂ
38 npcan ⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
39 36 37 38 sylancl ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
40 39 fveq2d ⊢ ( 𝜑 → ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) = ( AP ‘ 𝐾 ) )
41 40 oveqd ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
42 29 nnnn0d ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
43 vdwapun ⊢ ( ( ( 𝐾 − 1 ) ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
44 42 6 7 43 syl3anc ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ ( ( 𝐾 − 1 ) + 1 ) ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
45 41 44 eqtr3d ⊢ ( 𝜑 → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) = ( { 𝐴 } ∪ ( ( 𝐴 + 𝐷 ) ( AP ‘ ( 𝐾 − 1 ) ) 𝐷 ) ) )
46 33 45 eleqtrrd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
47 26 46 sseldd ⊢ ( 𝜑 → ( 𝐴 + 𝐷 ) ∈ ( 1 ... 𝑊 ) )
48 elfzuz3 ⊢ ( ( 𝐴 + 𝐷 ) ∈ ( 1 ... 𝑊 ) → 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + 𝐷 ) ) )
49 uznn0sub ⊢ ( 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + 𝐷 ) ) → ( 𝑊 − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
50 47 48 49 3syl ⊢ ( 𝜑 → ( 𝑊 − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 )
51 nnnn0addcl ⊢ ( ( ( 𝐴 + 𝐴 ) ∈ ℕ ∧ ( 𝑊 − ( 𝐴 + 𝐷 ) ) ∈ ℕ0 ) → ( ( 𝐴 + 𝐴 ) + ( 𝑊 − ( 𝐴 + 𝐷 ) ) ) ∈ ℕ )
52 21 50 51 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 + 𝐴 ) + ( 𝑊 − ( 𝐴 + 𝐷 ) ) ) ∈ ℕ )
53 20 52 eqeltrrd ⊢ ( 𝜑 → ( 𝐴 + ( 𝑊 − 𝐷 ) ) ∈ ℕ )
54 1nn ⊢ 1 ∈ ℕ
55 f1osng ⊢ ( ( 1 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → { ⟨ 1 , 𝐷 ⟩ } : { 1 } –1-1-onto→ { 𝐷 } )
56 54 7 55 sylancr ⊢ ( 𝜑 → { ⟨ 1 , 𝐷 ⟩ } : { 1 } –1-1-onto→ { 𝐷 } )
57 f1of ⊢ ( { ⟨ 1 , 𝐷 ⟩ } : { 1 } –1-1-onto→ { 𝐷 } → { ⟨ 1 , 𝐷 ⟩ } : { 1 } ⟶ { 𝐷 } )
58 56 57 syl ⊢ ( 𝜑 → { ⟨ 1 , 𝐷 ⟩ } : { 1 } ⟶ { 𝐷 } )
59 7 snssd ⊢ ( 𝜑 → { 𝐷 } ⊆ ℕ )
60 58 59 fssd ⊢ ( 𝜑 → { ⟨ 1 , 𝐷 ⟩ } : { 1 } ⟶ ℕ )
61 1z ⊢ 1 ∈ ℤ
62 fzsn ⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
63 61 62 ax-mp ⊢ ( 1 ... 1 ) = { 1 }
64 63 feq2i ⊢ ( { ⟨ 1 , 𝐷 ⟩ } : ( 1 ... 1 ) ⟶ ℕ ↔ { ⟨ 1 , 𝐷 ⟩ } : { 1 } ⟶ ℕ )
65 60 64 sylibr ⊢ ( 𝜑 → { ⟨ 1 , 𝐷 ⟩ } : ( 1 ... 1 ) ⟶ ℕ )
66 nnex ⊢ ℕ ∈ V
67 ovex ⊢ ( 1 ... 1 ) ∈ V
68 66 67 elmap ⊢ ( { ⟨ 1 , 𝐷 ⟩ } ∈ ( ℕ ↑m ( 1 ... 1 ) ) ↔ { ⟨ 1 , 𝐷 ⟩ } : ( 1 ... 1 ) ⟶ ℕ )
69 65 68 sylibr ⊢ ( 𝜑 → { ⟨ 1 , 𝐷 ⟩ } ∈ ( ℕ ↑m ( 1 ... 1 ) ) )
70 6 3 nnaddcld ⊢ ( 𝜑 → ( 𝐴 + 𝑊 ) ∈ ℕ )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 + 𝑊 ) ∈ ℕ )
72 elfznn0 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑚 ∈ ℕ0 )
73 7 nnnn0d ⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
74 nn0mulcl ⊢ ( ( 𝑚 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ) → ( 𝑚 · 𝐷 ) ∈ ℕ0 )
75 72 73 74 syl2anr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 · 𝐷 ) ∈ ℕ0 )
76 nnnn0addcl ⊢ ( ( ( 𝐴 + 𝑊 ) ∈ ℕ ∧ ( 𝑚 · 𝐷 ) ∈ ℕ0 ) → ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ℕ )
77 71 75 76 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ℕ )
78 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
79 77 78 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( ℤ≥ ‘ 1 ) )
80 8 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐺 “ { 𝐶 } ) )
81 eqid ⊢ ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑚 · 𝐷 ) )
82 oveq1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 · 𝐷 ) = ( 𝑚 · 𝐷 ) )
83 82 oveq2d ⊢ ( 𝑛 = 𝑚 → ( 𝐴 + ( 𝑛 · 𝐷 ) ) = ( 𝐴 + ( 𝑚 · 𝐷 ) ) )
84 83 rspceeqv ⊢ ( ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) )
85 81 84 mpan2 ⊢ ( 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) → ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) )
86 35 nnnn0d ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
87 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
88 86 6 7 87 syl3anc ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) )
89 88 biimpar ⊢ ( ( 𝜑 ∧ ∃ 𝑛 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐴 + ( 𝑚 · 𝐷 ) ) = ( 𝐴 + ( 𝑛 · 𝐷 ) ) ) → ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
90 85 89 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
91 80 90 sseldd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( ◡ 𝐺 “ { 𝐶 } ) )
92 23 9 fnmpti ⊢ 𝐺 Fn ( 1 ... 𝑊 )
93 fniniseg ⊢ ( 𝐺 Fn ( 1 ... 𝑊 ) → ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( ◡ 𝐺 “ { 𝐶 } ) ↔ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) ) )
94 92 93 ax-mp ⊢ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( ◡ 𝐺 “ { 𝐶 } ) ↔ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) )
95 91 94 sylib ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) )
96 95 simpld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) )
97 elfzuz3 ⊢ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) → 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) )
98 eluzelz ⊢ ( 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) → 𝑊 ∈ ℤ )
99 eluzadd ⊢ ( ( 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) ∧ 𝑊 ∈ ℤ ) → ( 𝑊 + 𝑊 ) ∈ ( ℤ≥ ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
100 98 99 mpdan ⊢ ( 𝑊 ∈ ( ℤ≥ ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) → ( 𝑊 + 𝑊 ) ∈ ( ℤ≥ ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
101 96 97 100 3syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑊 + 𝑊 ) ∈ ( ℤ≥ ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
102 14 2timesd ⊢ ( 𝜑 → ( 2 · 𝑊 ) = ( 𝑊 + 𝑊 ) )
103 102 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 2 · 𝑊 ) = ( 𝑊 + 𝑊 ) )
104 10 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐴 ∈ ℂ )
105 14 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑊 ∈ ℂ )
106 75 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑚 · 𝐷 ) ∈ ℂ )
107 104 105 106 add32d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) = ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) )
108 107 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ℤ≥ ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = ( ℤ≥ ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
109 101 103 108 3eltr4d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 2 · 𝑊 ) ∈ ( ℤ≥ ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) )
110 elfzuzb ⊢ ( ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... ( 2 · 𝑊 ) ) ↔ ( ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( 2 · 𝑊 ) ∈ ( ℤ≥ ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) ) )
111 79 109 110 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... ( 2 · 𝑊 ) ) )
112 107 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
113 fvoveq1 ⊢ ( 𝑥 = ( 𝐴 + ( 𝑚 · 𝐷 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑊 ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
114 fvex ⊢ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) ∈ V
115 113 9 114 fvmpt ⊢ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... 𝑊 ) → ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
116 96 115 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑚 · 𝐷 ) ) + 𝑊 ) ) )
117 95 simprd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐺 ‘ ( 𝐴 + ( 𝑚 · 𝐷 ) ) ) = 𝐶 )
118 112 116 117 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐹 ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = 𝐶 )
119 111 118 jca ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) )
120 eleq1 ⊢ ( 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) → ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ↔ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... ( 2 · 𝑊 ) ) ) )
121 fveqeq2 ⊢ ( 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) → ( ( 𝐹 ‘ 𝑥 ) = 𝐶 ↔ ( 𝐹 ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) )
122 120 121 anbi12d ⊢ ( 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) → ( ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ↔ ( ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) = 𝐶 ) ) )
123 119 122 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) → ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
124 123 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) → ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
125 vdwapval ⊢ ( ( 𝐾 ∈ ℕ0 ∧ ( 𝐴 + 𝑊 ) ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( 𝑥 ∈ ( ( 𝐴 + 𝑊 ) ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) )
126 86 70 7 125 syl3anc ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 + 𝑊 ) ( AP ‘ 𝐾 ) 𝐷 ) ↔ ∃ 𝑚 ∈ ( 0 ... ( 𝐾 − 1 ) ) 𝑥 = ( ( 𝐴 + 𝑊 ) + ( 𝑚 · 𝐷 ) ) ) )
127 ffn ⊢ ( 𝐹 : ( 1 ... ( 2 · 𝑊 ) ) ⟶ 𝑅 → 𝐹 Fn ( 1 ... ( 2 · 𝑊 ) ) )
128 fniniseg ⊢ ( 𝐹 Fn ( 1 ... ( 2 · 𝑊 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝐶 } ) ↔ ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
129 4 127 128 3syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 𝐶 } ) ↔ ( 𝑥 ∈ ( 1 ... ( 2 · 𝑊 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = 𝐶 ) ) )
130 124 126 129 3imtr4d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( 𝐴 + 𝑊 ) ( AP ‘ 𝐾 ) 𝐷 ) → 𝑥 ∈ ( ◡ 𝐹 “ { 𝐶 } ) ) )
131 130 ssrdv ⊢ ( 𝜑 → ( ( 𝐴 + 𝑊 ) ( AP ‘ 𝐾 ) 𝐷 ) ⊆ ( ◡ 𝐹 “ { 𝐶 } ) )
132 fvsng ⊢ ( ( 1 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) = 𝐷 )
133 54 7 132 sylancr ⊢ ( 𝜑 → ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) = 𝐷 )
134 133 oveq2d ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) = ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + 𝐷 ) )
135 10 18 11 addassd ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + 𝐷 ) = ( 𝐴 + ( ( 𝑊 − 𝐷 ) + 𝐷 ) ) )
136 14 11 npcand ⊢ ( 𝜑 → ( ( 𝑊 − 𝐷 ) + 𝐷 ) = 𝑊 )
137 136 oveq2d ⊢ ( 𝜑 → ( 𝐴 + ( ( 𝑊 − 𝐷 ) + 𝐷 ) ) = ( 𝐴 + 𝑊 ) )
138 134 135 137 3eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) = ( 𝐴 + 𝑊 ) )
139 138 133 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) = ( ( 𝐴 + 𝑊 ) ( AP ‘ 𝐾 ) 𝐷 ) )
140 138 fveq2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) = ( 𝐹 ‘ ( 𝐴 + 𝑊 ) ) )
141 vdwapid1 ⊢ ( ( 𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ ) → 𝐴 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
142 35 6 7 141 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 ( AP ‘ 𝐾 ) 𝐷 ) )
143 8 142 sseldd ⊢ ( 𝜑 → 𝐴 ∈ ( ◡ 𝐺 “ { 𝐶 } ) )
144 fniniseg ⊢ ( 𝐺 Fn ( 1 ... 𝑊 ) → ( 𝐴 ∈ ( ◡ 𝐺 “ { 𝐶 } ) ↔ ( 𝐴 ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ 𝐴 ) = 𝐶 ) ) )
145 92 144 ax-mp ⊢ ( 𝐴 ∈ ( ◡ 𝐺 “ { 𝐶 } ) ↔ ( 𝐴 ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ 𝐴 ) = 𝐶 ) )
146 143 145 sylib ⊢ ( 𝜑 → ( 𝐴 ∈ ( 1 ... 𝑊 ) ∧ ( 𝐺 ‘ 𝐴 ) = 𝐶 ) )
147 146 simpld ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑊 ) )
148 fvoveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ ( 𝑥 + 𝑊 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝑊 ) ) )
149 fvex ⊢ ( 𝐹 ‘ ( 𝐴 + 𝑊 ) ) ∈ V
150 148 9 149 fvmpt ⊢ ( 𝐴 ∈ ( 1 ... 𝑊 ) → ( 𝐺 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐴 + 𝑊 ) ) )
151 147 150 syl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = ( 𝐹 ‘ ( 𝐴 + 𝑊 ) ) )
152 146 simprd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = 𝐶 )
153 140 151 152 3eqtr2d ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) = 𝐶 )
154 153 sneqd ⊢ ( 𝜑 → { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } = { 𝐶 } )
155 154 imaeq2d ⊢ ( 𝜑 → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) = ( ◡ 𝐹 “ { 𝐶 } ) )
156 131 139 155 3sstr4d ⊢ ( 𝜑 → ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) )
157 156 ralrimivw ⊢ ( 𝜑 → ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) )
158 153 mpteq2dv ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) = ( 𝑖 ∈ ( 1 ... 1 ) ↦ 𝐶 ) )
159 fconstmpt ⊢ ( ( 1 ... 1 ) × { 𝐶 } ) = ( 𝑖 ∈ ( 1 ... 1 ) ↦ 𝐶 )
160 158 159 eqtr4di ⊢ ( 𝜑 → ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) = ( ( 1 ... 1 ) × { 𝐶 } ) )
161 160 rneqd ⊢ ( 𝜑 → ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) = ran ( ( 1 ... 1 ) × { 𝐶 } ) )
162 elfz3 ⊢ ( 1 ∈ ℤ → 1 ∈ ( 1 ... 1 ) )
163 ne0i ⊢ ( 1 ∈ ( 1 ... 1 ) → ( 1 ... 1 ) ≠ ∅ )
164 61 162 163 mp2b ⊢ ( 1 ... 1 ) ≠ ∅
165 rnxp ⊢ ( ( 1 ... 1 ) ≠ ∅ → ran ( ( 1 ... 1 ) × { 𝐶 } ) = { 𝐶 } )
166 164 165 ax-mp ⊢ ran ( ( 1 ... 1 ) × { 𝐶 } ) = { 𝐶 }
167 161 166 eqtrdi ⊢ ( 𝜑 → ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) = { 𝐶 } )
168 167 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) ) = ( ♯ ‘ { 𝐶 } ) )
169 hashsng ⊢ ( 𝐶 ∈ V → ( ♯ ‘ { 𝐶 } ) = 1 )
170 5 169 ax-mp ⊢ ( ♯ ‘ { 𝐶 } ) = 1
171 168 170 eqtrdi ⊢ ( 𝜑 → ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) ) = 1 )
172 oveq1 ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) )
173 172 oveq1d ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) = ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) )
174 fvoveq1 ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) )
175 174 sneqd ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } = { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } )
176 175 imaeq2d ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) )
177 173 176 sseq12d ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) )
178 177 ralbidv ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ) )
179 174 mpteq2dv ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) )
180 179 rneqd ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) = ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) )
181 180 fveqeq2d ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ↔ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) )
182 178 181 anbi12d ⊢ ( 𝑎 = ( 𝐴 + ( 𝑊 − 𝐷 ) ) → ( ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) ) )
183 fveq1 ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ( 𝑑 ‘ 𝑖 ) = ( { ⟨ 1 , 𝐷 ⟩ } ‘ 𝑖 ) )
184 elfz1eq ⊢ ( 𝑖 ∈ ( 1 ... 1 ) → 𝑖 = 1 )
185 184 fveq2d ⊢ ( 𝑖 ∈ ( 1 ... 1 ) → ( { ⟨ 1 , 𝐷 ⟩ } ‘ 𝑖 ) = ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) )
186 183 185 sylan9eq ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( 𝑑 ‘ 𝑖 ) = ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) )
187 186 oveq2d ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) = ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) )
188 187 186 oveq12d ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) = ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) )
189 187 fveq2d ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) )
190 189 sneqd ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } = { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } )
191 190 imaeq2d ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) = ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) )
192 188 191 sseq12d ⊢ ( ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } ∧ 𝑖 ∈ ( 1 ... 1 ) ) → ( ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) ) )
193 192 ralbidva ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ↔ ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) ) )
194 189 mpteq2dva ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) = ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) )
195 194 rneqd ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) = ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) )
196 195 fveqeq2d ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ( ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ↔ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) ) = 1 ) )
197 193 196 anbi12d ⊢ ( 𝑑 = { ⟨ 1 , 𝐷 ⟩ } → ( ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) ↔ ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) ) = 1 ) ) )
198 182 197 rspc2ev ⊢ ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) ∈ ℕ ∧ { ⟨ 1 , 𝐷 ⟩ } ∈ ( ℕ ↑m ( 1 ... 1 ) ) ∧ ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ( AP ‘ 𝐾 ) ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( ( 𝐴 + ( 𝑊 − 𝐷 ) ) + ( { ⟨ 1 , 𝐷 ⟩ } ‘ 1 ) ) ) ) ) = 1 ) ) → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 1 ) ) ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) )
199 53 69 157 171 198 syl112anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 1 ) ) ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) )
200 ovex ⊢ ( 1 ... ( 2 · 𝑊 ) ) ∈ V
201 54 a1i ⊢ ( 𝜑 → 1 ∈ ℕ )
202 eqid ⊢ ( 1 ... 1 ) = ( 1 ... 1 )
203 200 86 4 201 202 vdwpc ⊢ ( 𝜑 → ( ⟨ 1 , 𝐾 ⟩ PolyAP 𝐹 ↔ ∃ 𝑎 ∈ ℕ ∃ 𝑑 ∈ ( ℕ ↑m ( 1 ... 1 ) ) ( ∀ 𝑖 ∈ ( 1 ... 1 ) ( ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ( AP ‘ 𝐾 ) ( 𝑑 ‘ 𝑖 ) ) ⊆ ( ◡ 𝐹 “ { ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) } ) ∧ ( ♯ ‘ ran ( 𝑖 ∈ ( 1 ... 1 ) ↦ ( 𝐹 ‘ ( 𝑎 + ( 𝑑 ‘ 𝑖 ) ) ) ) ) = 1 ) ) )
204 199 203 mpbird ⊢ ( 𝜑 → ⟨ 1 , 𝐾 ⟩ PolyAP 𝐹 )