Definition df-plylt 42607

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 42605	. 2 class Poly<
2		vs	. . 3 setvar 𝑠
3		vx	. . 3 setvar 𝑥
4		cc 11146	. . . 4 class ℂ
5	4	cpw 4606	. . 3 class 𝒫 ℂ
6		cn0 12512	. . 3 class ℕ0
7		vp	. . . . . . 7 setvar 𝑝
8	7	cv 1532	. . . . . 6 class 𝑝
9		c0p 25626	. . . . . 6 class 0𝑝
10	8, 9	wceq 1533	. . . . 5 wff 𝑝 = 0𝑝
11		cdgr 26149	. . . . . . 7 class deg
12	8, 11	cfv 6553	. . . . . 6 class (deg‘𝑝)
13	3	cv 1532	. . . . . 6 class 𝑥
14		clt 11288	. . . . . 6 class <
15	12, 13, 14	wbr 5152	. . . . 5 wff (deg‘𝑝) < 𝑥
16	10, 15	wo 845	. . . 4 wff (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)
17	2	cv 1532	. . . . 5 class 𝑠
18		cply 26146	. . . . 5 class Poly
19	17, 18	cfv 6553	. . . 4 class (Poly‘𝑠)
20	16, 7, 19	crab 3430	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}
21	2, 3, 5, 6, 20	cmpo 7428	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
22	1, 21	wceq 1533	1 wff Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})

This definition is referenced by: (None)