Definition df-plylt

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplylt	|- Poly<
1		vs	|- s
2		cc	|- CC
3	2	cpw	|- ~P CC
4		vx	|- x
5		cn0	|- NN0
6		vp	|- p
7		cply	|- Poly
8	1	cv	|- s
9	8 7	cfv	|- ( Poly ` s )
10	6	cv	|- p
11		c0p	|- 0p
12	10 11	wceq	|- p = 0p
13		cdgr	|- deg
14	10 13	cfv	|- ( deg ` p )
15		clt	|- <
16	4	cv	|- x
17	14 16 15	wbr	|- ( deg ` p ) < x
18	12 17	wo	|- ( p = 0p \/ ( deg ` p ) < x )
19	18 6 9	crab	|- { p e. ( Poly ` s ) | ( p = 0p \/ ( deg ` p ) < x ) }
20	1 4 3 5 19	cmpo	|- ( s e. ~P CC , x e. NN0 |-> { p e. ( Poly ` s ) | ( p = 0p \/ ( deg ` p ) < x ) } )
21	0 20	wceq	|- Poly< = ( s e. ~P CC , x e. NN0 |-> { p e. ( Poly ` s ) | ( p = 0p \/ ( deg ` p ) < x ) } )