Definition df-plylt 43146

Description: Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)

Assertion

Ref	Expression
df-plylt	⊢ Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})

Distinct variable group:   𝑠,𝑝,𝑥

Detailed syntax breakdown of Definition df-plylt

Step	Hyp	Ref	Expression
1		cplylt 43144	. 2 class Poly<
2		vs	. . 3 setvar 𝑠
3		vx	. . 3 setvar 𝑥
4		cc 11153	. . . 4 class ℂ
5	4	cpw 4600	. . 3 class 𝒫 ℂ
6		cn0 12526	. . 3 class ℕ0
7		vp	. . . . . . 7 setvar 𝑝
8	7	cv 1539	. . . . . 6 class 𝑝
9		c0p 25704	. . . . . 6 class 0𝑝
10	8, 9	wceq 1540	. . . . 5 wff 𝑝 = 0𝑝
11		cdgr 26226	. . . . . . 7 class deg
12	8, 11	cfv 6561	. . . . . 6 class (deg‘𝑝)
13	3	cv 1539	. . . . . 6 class 𝑥
14		clt 11295	. . . . . 6 class <
15	12, 13, 14	wbr 5143	. . . . 5 wff (deg‘𝑝) < 𝑥
16	10, 15	wo 848	. . . 4 wff (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)
17	2	cv 1539	. . . . 5 class 𝑠
18		cply 26223	. . . . 5 class Poly
19	17, 18	cfv 6561	. . . 4 class (Poly‘𝑠)
20	16, 7, 19	crab 3436	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}
21	2, 3, 5, 6, 20	cmpo 7433	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
22	1, 21	wceq 1540	1 wff Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})

This definition is referenced by: (None)