Definition df-plylt

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

	Ref	Expression
Assertion	df-plylt	$$⊢{\mathrm{Poly}}_{<}=\left(s\in 𝒫ℂ,x\in {\mathbb{N}}_0⟼\left\{p\in \mathrm{Poly}\left(s\right)|\left(p=0_{𝑝}\vee \mathrm{deg}\left(p\right)<x\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplylt	$$class{\mathrm{Poly}}_{<}$$
1		vs	$$setvars$$
2		cc	$$classℂ$$
3	2	cpw	$$class𝒫ℂ$$
4		vx	$$setvarx$$
5		cn0	$$class{\mathbb{N}}_0$$
6		vp	$$setvarp$$
7		cply	$$class\mathrm{Poly}$$
8	1	cv	$$setvars$$
9	8 7	cfv	$$class\mathrm{Poly}\left(s\right)$$
10	6	cv	$$setvarp$$
11		c0p	$$class{0}_{𝑝}$$
12	10 11	wceq	$$wffp=0_{𝑝}$$
13		cdgr	$$class\mathrm{deg}$$
14	10 13	cfv	$$class\mathrm{deg}\left(p\right)$$
15		clt	$$class<$$
16	4	cv	$$setvarx$$
17	14 16 15	wbr	$$wff\mathrm{deg}\left(p\right)<x$$
18	12 17	wo	$$wff\left(p=0_{𝑝}\vee \mathrm{deg}\left(p\right)<x\right)$$
19	18 6 9	crab	$$class\left\{p\in \mathrm{Poly}\left(s\right)|\left(p=0_{𝑝}\vee \mathrm{deg}\left(p\right)<x\right)\right\}$$
20	1 4 3 5 19	cmpo	$$class\left(s\in 𝒫ℂ,x\in {\mathbb{N}}_0⟼\left\{p\in \mathrm{Poly}\left(s\right)|\left(p=0_{𝑝}\vee \mathrm{deg}\left(p\right)<x\right)\right\}\right)$$
21	0 20	wceq	$$wff{\mathrm{Poly}}_{<}=\left(s\in 𝒫ℂ,x\in {\mathbb{N}}_0⟼\left\{p\in \mathrm{Poly}\left(s\right)|\left(p=0_{𝑝}\vee \mathrm{deg}\left(p\right)<x\right)\right\}\right)$$