Detailed syntax breakdown of Definition df-plylt
Step | Hyp | Ref
| Expression |
1 | | cplylt 40946 |
. 2
class
Poly< |
2 | | vs |
. . 3
setvar 𝑠 |
3 | | vx |
. . 3
setvar 𝑥 |
4 | | cc 10862 |
. . . 4
class
ℂ |
5 | 4 | cpw 4539 |
. . 3
class 𝒫
ℂ |
6 | | cn0 12225 |
. . 3
class
ℕ0 |
7 | | vp |
. . . . . . 7
setvar 𝑝 |
8 | 7 | cv 1541 |
. . . . . 6
class 𝑝 |
9 | | c0p 24823 |
. . . . . 6
class
0𝑝 |
10 | 8, 9 | wceq 1542 |
. . . . 5
wff 𝑝 =
0𝑝 |
11 | | cdgr 25338 |
. . . . . . 7
class
deg |
12 | 8, 11 | cfv 6431 |
. . . . . 6
class
(deg‘𝑝) |
13 | 3 | cv 1541 |
. . . . . 6
class 𝑥 |
14 | | clt 11002 |
. . . . . 6
class
< |
15 | 12, 13, 14 | wbr 5079 |
. . . . 5
wff
(deg‘𝑝) <
𝑥 |
16 | 10, 15 | wo 844 |
. . . 4
wff (𝑝 = 0𝑝 ∨
(deg‘𝑝) < 𝑥) |
17 | 2 | cv 1541 |
. . . . 5
class 𝑠 |
18 | | cply 25335 |
. . . . 5
class
Poly |
19 | 17, 18 | cfv 6431 |
. . . 4
class
(Poly‘𝑠) |
20 | 16, 7, 19 | crab 3070 |
. . 3
class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨
(deg‘𝑝) < 𝑥)} |
21 | 2, 3, 5, 6, 20 | cmpo 7271 |
. 2
class (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0
↦ {𝑝 ∈
(Poly‘𝑠) ∣
(𝑝 = 0𝑝
∨ (deg‘𝑝) <
𝑥)}) |
22 | 1, 21 | wceq 1542 |
1
wff
Poly< = (𝑠
∈ 𝒫 ℂ, 𝑥
∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨
(deg‘𝑝) < 𝑥)}) |