Detailed syntax breakdown of Definition df-vdwpc
Step | Hyp | Ref
| Expression |
1 | | cvdwp 16678 |
. 2
class
PolyAP |
2 | | va |
. . . . . . . . . . 11
setvar 𝑎 |
3 | 2 | cv 1538 |
. . . . . . . . . 10
class 𝑎 |
4 | | vi |
. . . . . . . . . . . 12
setvar 𝑖 |
5 | 4 | cv 1538 |
. . . . . . . . . . 11
class 𝑖 |
6 | | vd |
. . . . . . . . . . . 12
setvar 𝑑 |
7 | 6 | cv 1538 |
. . . . . . . . . . 11
class 𝑑 |
8 | 5, 7 | cfv 6426 |
. . . . . . . . . 10
class (𝑑‘𝑖) |
9 | | caddc 10884 |
. . . . . . . . . 10
class
+ |
10 | 3, 8, 9 | co 7267 |
. . . . . . . . 9
class (𝑎 + (𝑑‘𝑖)) |
11 | | vk |
. . . . . . . . . . 11
setvar 𝑘 |
12 | 11 | cv 1538 |
. . . . . . . . . 10
class 𝑘 |
13 | | cvdwa 16676 |
. . . . . . . . . 10
class
AP |
14 | 12, 13 | cfv 6426 |
. . . . . . . . 9
class
(AP‘𝑘) |
15 | 10, 8, 14 | co 7267 |
. . . . . . . 8
class ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) |
16 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
17 | 16 | cv 1538 |
. . . . . . . . . 10
class 𝑓 |
18 | 17 | ccnv 5583 |
. . . . . . . . 9
class ◡𝑓 |
19 | 10, 17 | cfv 6426 |
. . . . . . . . . 10
class (𝑓‘(𝑎 + (𝑑‘𝑖))) |
20 | 19 | csn 4561 |
. . . . . . . . 9
class {(𝑓‘(𝑎 + (𝑑‘𝑖)))} |
21 | 18, 20 | cima 5587 |
. . . . . . . 8
class (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
22 | 15, 21 | wss 3886 |
. . . . . . 7
wff ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
23 | | c1 10882 |
. . . . . . . 8
class
1 |
24 | | vm |
. . . . . . . . 9
setvar 𝑚 |
25 | 24 | cv 1538 |
. . . . . . . 8
class 𝑚 |
26 | | cfz 13249 |
. . . . . . . 8
class
... |
27 | 23, 25, 26 | co 7267 |
. . . . . . 7
class
(1...𝑚) |
28 | 22, 4, 27 | wral 3064 |
. . . . . 6
wff
∀𝑖 ∈
(1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
29 | 4, 27, 19 | cmpt 5156 |
. . . . . . . . 9
class (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))) |
30 | 29 | crn 5585 |
. . . . . . . 8
class ran
(𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))) |
31 | | chash 14054 |
. . . . . . . 8
class
♯ |
32 | 30, 31 | cfv 6426 |
. . . . . . 7
class
(♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) |
33 | 32, 25 | wceq 1539 |
. . . . . 6
wff
(♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚 |
34 | 28, 33 | wa 396 |
. . . . 5
wff
(∀𝑖 ∈
(1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
35 | | cn 11983 |
. . . . . 6
class
ℕ |
36 | | cmap 8602 |
. . . . . 6
class
↑m |
37 | 35, 27, 36 | co 7267 |
. . . . 5
class (ℕ
↑m (1...𝑚)) |
38 | 34, 6, 37 | wrex 3065 |
. . . 4
wff
∃𝑑 ∈
(ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
39 | 38, 2, 35 | wrex 3065 |
. . 3
wff
∃𝑎 ∈
ℕ ∃𝑑 ∈
(ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
40 | 39, 24, 11, 16 | coprab 7268 |
. 2
class
{〈〈𝑚,
𝑘〉, 𝑓〉 ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)} |
41 | 1, 40 | wceq 1539 |
1
wff PolyAP =
{〈〈𝑚, 𝑘〉, 𝑓〉 ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)} |