Detailed syntax breakdown of Definition df-vdwpc
Step | Hyp | Ref
| Expression |
1 | | cvdwp 16293 |
. 2
class
PolyAP |
2 | | va |
. . . . . . . . . . 11
setvar 𝑎 |
3 | 2 | cv 1537 |
. . . . . . . . . 10
class 𝑎 |
4 | | vi |
. . . . . . . . . . . 12
setvar 𝑖 |
5 | 4 | cv 1537 |
. . . . . . . . . . 11
class 𝑖 |
6 | | vd |
. . . . . . . . . . . 12
setvar 𝑑 |
7 | 6 | cv 1537 |
. . . . . . . . . . 11
class 𝑑 |
8 | 5, 7 | cfv 6324 |
. . . . . . . . . 10
class (𝑑‘𝑖) |
9 | | caddc 10529 |
. . . . . . . . . 10
class
+ |
10 | 3, 8, 9 | co 7135 |
. . . . . . . . 9
class (𝑎 + (𝑑‘𝑖)) |
11 | | vk |
. . . . . . . . . . 11
setvar 𝑘 |
12 | 11 | cv 1537 |
. . . . . . . . . 10
class 𝑘 |
13 | | cvdwa 16291 |
. . . . . . . . . 10
class
AP |
14 | 12, 13 | cfv 6324 |
. . . . . . . . 9
class
(AP‘𝑘) |
15 | 10, 8, 14 | co 7135 |
. . . . . . . 8
class ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) |
16 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
17 | 16 | cv 1537 |
. . . . . . . . . 10
class 𝑓 |
18 | 17 | ccnv 5518 |
. . . . . . . . 9
class ◡𝑓 |
19 | 10, 17 | cfv 6324 |
. . . . . . . . . 10
class (𝑓‘(𝑎 + (𝑑‘𝑖))) |
20 | 19 | csn 4525 |
. . . . . . . . 9
class {(𝑓‘(𝑎 + (𝑑‘𝑖)))} |
21 | 18, 20 | cima 5522 |
. . . . . . . 8
class (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
22 | 15, 21 | wss 3881 |
. . . . . . 7
wff ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
23 | | c1 10527 |
. . . . . . . 8
class
1 |
24 | | vm |
. . . . . . . . 9
setvar 𝑚 |
25 | 24 | cv 1537 |
. . . . . . . 8
class 𝑚 |
26 | | cfz 12885 |
. . . . . . . 8
class
... |
27 | 23, 25, 26 | co 7135 |
. . . . . . 7
class
(1...𝑚) |
28 | 22, 4, 27 | wral 3106 |
. . . . . 6
wff
∀𝑖 ∈
(1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) |
29 | 4, 27, 19 | cmpt 5110 |
. . . . . . . . 9
class (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))) |
30 | 29 | crn 5520 |
. . . . . . . 8
class ran
(𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))) |
31 | | chash 13686 |
. . . . . . . 8
class
♯ |
32 | 30, 31 | cfv 6324 |
. . . . . . 7
class
(♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) |
33 | 32, 25 | wceq 1538 |
. . . . . 6
wff
(♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚 |
34 | 28, 33 | wa 399 |
. . . . 5
wff
(∀𝑖 ∈
(1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
35 | | cn 11625 |
. . . . . 6
class
ℕ |
36 | | cmap 8389 |
. . . . . 6
class
↑m |
37 | 35, 27, 36 | co 7135 |
. . . . 5
class (ℕ
↑m (1...𝑚)) |
38 | 34, 6, 37 | wrex 3107 |
. . . 4
wff
∃𝑑 ∈
(ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
39 | 38, 2, 35 | wrex 3107 |
. . 3
wff
∃𝑎 ∈
ℕ ∃𝑑 ∈
(ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚) |
40 | 39, 24, 11, 16 | coprab 7136 |
. 2
class
{〈〈𝑚,
𝑘〉, 𝑓〉 ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)} |
41 | 1, 40 | wceq 1538 |
1
wff PolyAP =
{〈〈𝑚, 𝑘〉, 𝑓〉 ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)} |