Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-plylt Structured version   Unicode version

Definition df-plylt 31251
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
StepHypRef Expression
1 cplylt 31249 . 2  class Poly<
2 vs . . 3  setvar  s
3 vx . . 3  setvar  x
4 cc 9401 . . . 4  class  CC
54cpw 3927 . . 3  class  ~P CC
6 cn0 10712 . . 3  class  NN0
7 vp . . . . . . 7  setvar  p
87cv 1398 . . . . . 6  class  p
9 c0p 22161 . . . . . 6  class  0p
108, 9wceq 1399 . . . . 5  wff  p  =  0p
11 cdgr 22669 . . . . . . 7  class deg
128, 11cfv 5496 . . . . . 6  class  (deg `  p )
133cv 1398 . . . . . 6  class  x
14 clt 9539 . . . . . 6  class  <
1512, 13, 14wbr 4367 . . . . 5  wff  (deg `  p )  <  x
1610, 15wo 366 . . . 4  wff  ( p  =  0p  \/  (deg `  p )  <  x )
172cv 1398 . . . . 5  class  s
18 cply 22666 . . . . 5  class Poly
1917, 18cfv 5496 . . . 4  class  (Poly `  s )
2016, 7, 19crab 2736 . . 3  class  { p  e.  (Poly `  s )  |  ( p  =  0p  \/  (deg `  p )  <  x
) }
212, 3, 5, 6, 20cmpt2 6198 . 2  class  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0p  \/  (deg `  p )  <  x
) } )
221, 21wceq 1399 1  wff Poly<  =  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0p  \/  (deg `  p )  <  x
) } )
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator