Definition df-plylt 40959

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 40957	. 2 class Poly<
2		vs	. . 3 setvar 𝑠
3		vx	. . 3 setvar 𝑥
4		cc 10869	. . . 4 class ℂ
5	4	cpw 4533	. . 3 class 𝒫 ℂ
6		cn0 12233	. . 3 class ℕ0
7		vp	. . . . . . 7 setvar 𝑝
8	7	cv 1538	. . . . . 6 class 𝑝
9		c0p 24833	. . . . . 6 class 0𝑝
10	8, 9	wceq 1539	. . . . 5 wff 𝑝 = 0𝑝
11		cdgr 25348	. . . . . . 7 class deg
12	8, 11	cfv 6433	. . . . . 6 class (deg‘𝑝)
13	3	cv 1538	. . . . . 6 class 𝑥
14		clt 11009	. . . . . 6 class <
15	12, 13, 14	wbr 5074	. . . . 5 wff (deg‘𝑝) < 𝑥
16	10, 15	wo 844	. . . 4 wff (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)
17	2	cv 1538	. . . . 5 class 𝑠
18		cply 25345	. . . . 5 class Poly
19	17, 18	cfv 6433	. . . 4 class (Poly‘𝑠)
20	16, 7, 19	crab 3068	. . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}
21	2, 3, 5, 6, 20	cmpo 7277	. 2 class (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})
22	1, 21	wceq 1539	1 wff Poly< = (𝑠 ∈ 𝒫 ℂ, 𝑥 ∈ ℕ0 ↦ {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)})

This definition is referenced by: (None)