Detailed syntax breakdown of Definition df-mzpcl
Step | Hyp | Ref
| Expression |
1 | | cmzpcl 40246 |
. 2
class
mzPolyCld |
2 | | vv |
. . 3
setvar 𝑣 |
3 | | cvv 3408 |
. . 3
class
V |
4 | | cz 12176 |
. . . . . . . . . 10
class
ℤ |
5 | 2 | cv 1542 |
. . . . . . . . . 10
class 𝑣 |
6 | | cmap 8508 |
. . . . . . . . . 10
class
↑m |
7 | 4, 5, 6 | co 7213 |
. . . . . . . . 9
class (ℤ
↑m 𝑣) |
8 | | vi |
. . . . . . . . . . 11
setvar 𝑖 |
9 | 8 | cv 1542 |
. . . . . . . . . 10
class 𝑖 |
10 | 9 | csn 4541 |
. . . . . . . . 9
class {𝑖} |
11 | 7, 10 | cxp 5549 |
. . . . . . . 8
class ((ℤ
↑m 𝑣)
× {𝑖}) |
12 | | vp |
. . . . . . . . 9
setvar 𝑝 |
13 | 12 | cv 1542 |
. . . . . . . 8
class 𝑝 |
14 | 11, 13 | wcel 2110 |
. . . . . . 7
wff ((ℤ
↑m 𝑣)
× {𝑖}) ∈ 𝑝 |
15 | 14, 8, 4 | wral 3061 |
. . . . . 6
wff
∀𝑖 ∈
ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 |
16 | | vx |
. . . . . . . . 9
setvar 𝑥 |
17 | | vj |
. . . . . . . . . . 11
setvar 𝑗 |
18 | 17 | cv 1542 |
. . . . . . . . . 10
class 𝑗 |
19 | 16 | cv 1542 |
. . . . . . . . . 10
class 𝑥 |
20 | 18, 19 | cfv 6380 |
. . . . . . . . 9
class (𝑥‘𝑗) |
21 | 16, 7, 20 | cmpt 5135 |
. . . . . . . 8
class (𝑥 ∈ (ℤ
↑m 𝑣)
↦ (𝑥‘𝑗)) |
22 | 21, 13 | wcel 2110 |
. . . . . . 7
wff (𝑥 ∈ (ℤ
↑m 𝑣)
↦ (𝑥‘𝑗)) ∈ 𝑝 |
23 | 22, 17, 5 | wral 3061 |
. . . . . 6
wff
∀𝑗 ∈
𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝 |
24 | 15, 23 | wa 399 |
. . . . 5
wff
(∀𝑖 ∈
ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) |
25 | | vf |
. . . . . . . . . . 11
setvar 𝑓 |
26 | 25 | cv 1542 |
. . . . . . . . . 10
class 𝑓 |
27 | | vg |
. . . . . . . . . . 11
setvar 𝑔 |
28 | 27 | cv 1542 |
. . . . . . . . . 10
class 𝑔 |
29 | | caddc 10732 |
. . . . . . . . . . 11
class
+ |
30 | 29 | cof 7467 |
. . . . . . . . . 10
class
∘f + |
31 | 26, 28, 30 | co 7213 |
. . . . . . . . 9
class (𝑓 ∘f + 𝑔) |
32 | 31, 13 | wcel 2110 |
. . . . . . . 8
wff (𝑓 ∘f + 𝑔) ∈ 𝑝 |
33 | | cmul 10734 |
. . . . . . . . . . 11
class
· |
34 | 33 | cof 7467 |
. . . . . . . . . 10
class
∘f · |
35 | 26, 28, 34 | co 7213 |
. . . . . . . . 9
class (𝑓 ∘f ·
𝑔) |
36 | 35, 13 | wcel 2110 |
. . . . . . . 8
wff (𝑓 ∘f ·
𝑔) ∈ 𝑝 |
37 | 32, 36 | wa 399 |
. . . . . . 7
wff ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝) |
38 | 37, 27, 13 | wral 3061 |
. . . . . 6
wff
∀𝑔 ∈
𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝) |
39 | 38, 25, 13 | wral 3061 |
. . . . 5
wff
∀𝑓 ∈
𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝) |
40 | 24, 39 | wa 399 |
. . . 4
wff
((∀𝑖 ∈
ℤ ((ℤ ↑m 𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝)) |
41 | 4, 7, 6 | co 7213 |
. . . . 5
class (ℤ
↑m (ℤ ↑m 𝑣)) |
42 | 41 | cpw 4513 |
. . . 4
class 𝒫
(ℤ ↑m (ℤ ↑m 𝑣)) |
43 | 40, 12, 42 | crab 3065 |
. . 3
class {𝑝 ∈ 𝒫 (ℤ
↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))} |
44 | 2, 3, 43 | cmpt 5135 |
. 2
class (𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ
↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |
45 | 1, 44 | wceq 1543 |
1
wff mzPolyCld =
(𝑣 ∈ V ↦ {𝑝 ∈ 𝒫 (ℤ
↑m (ℤ ↑m 𝑣)) ∣ ((∀𝑖 ∈ ℤ ((ℤ ↑m
𝑣) × {𝑖}) ∈ 𝑝 ∧ ∀𝑗 ∈ 𝑣 (𝑥 ∈ (ℤ ↑m 𝑣) ↦ (𝑥‘𝑗)) ∈ 𝑝) ∧ ∀𝑓 ∈ 𝑝 ∀𝑔 ∈ 𝑝 ((𝑓 ∘f + 𝑔) ∈ 𝑝 ∧ (𝑓 ∘f · 𝑔) ∈ 𝑝))}) |