Definition df-plylt 36723

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 36721	. 2 class Poly<
2		vs	. . 3 setvar 𝑠
3		vx	. . 3 setvar 𝑥
4		cc 9813	. . . 4 class ℂ
5	4	cpw 4108	. . 3 class 𝒫 ℂ
6		cn0 11169	. . 3 class ℕ0
7		vp	. . . . . . 7 setvar 𝑝
8	7	cv 1474	. . . . . 6 class 𝑝
9		c0p 23242	. . . . . 6 class 0𝑝
10	8, 9	wceq 1475	. . . . 5 wff 𝑝 = 0𝑝
11		cdgr 23747	. . . . . . 7 class deg
12	8, 11	cfv 5804	. . . . . 6 class (deg‘𝑝)
13	3	cv 1474	. . . . . 6 class 𝑥
14		clt 9953	. . . . . 6 class <
15	12, 13, 14	wbr 4583	. . . . 5 wff (deg‘𝑝) < 𝑥
16	10, 15	wo 382	. . . 4 wff (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)
17	2	cv 1474	. . . . 5 class 𝑠
18		cply 23744	. . . . 5 class Poly
19	17, 18	cfv 5804	. . . 4 class (Poly‘𝑠)
20	16, 7, 19	crab 2900	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}
21	2, 3, 5, 6, 20	cmpt2 6551	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
22	1, 21	wceq 1475	1 wff Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})

This definition is referenced by: (None)