Definition df-plylt 37704

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

Assertion

Ref	Expression
df-plylt	|- Poly< = ( s e. ~P CC , x e. NN0 |-> { p e. (Poly ` s ) | ( p = 0p \/ (deg ` p ) < x ) } )

Distinct variable group:   s, p, x

Detailed syntax breakdown of Definition df-plylt

Step	Hyp	Ref	Expression
1		cplylt 37702	. 2 class Poly<
2		vs	. . 3 setvar s
3		vx	. . 3 setvar x
4		cc 9934	. . . 4 class CC
5	4	cpw 4158	. . 3 class ~P CC
6		cn0 11292	. . 3 class NN0
7		vp	. . . . . . 7 setvar p
8	7	cv 1482	. . . . . 6 class p
9		c0p 23436	. . . . . 6 class 0p
10	8, 9	wceq 1483	. . . . 5 wff p = 0p
11		cdgr 23943	. . . . . . 7 class deg
12	8, 11	cfv 5888	. . . . . 6 class (deg ` p )
13	3	cv 1482	. . . . . 6 class x
14		clt 10074	. . . . . 6 class <
15	12, 13, 14	wbr 4653	. . . . 5 wff (deg ` p ) < x
16	10, 15	wo 383	. . . 4 wff ( p = 0p \/ (deg ` p ) < x )
17	2	cv 1482	. . . . 5 class s
18		cply 23940	. . . . 5 class Poly
19	17, 18	cfv 5888	. . . 4 class (Poly ` s )
20	16, 7, 19	crab 2916	. . 3 class { p e. (Poly ` s ) | ( p = 0p \/ (deg ` p ) < x ) }
21	2, 3, 5, 6, 20	cmpt2 6652	. 2 class ( s e. ~P CC , x e. NN0 |-> { p e. (Poly ` s ) | ( p = 0p \/ (deg ` p ) < x ) } )
22	1, 21	wceq 1483	1 wff Poly< = ( s e. ~P CC , x e. NN0 |-> { p e. (Poly ` s ) | ( p = 0p \/ (deg ` p ) < x ) } )

This definition is referenced by: (None)