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 29639
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 29637 . 2  class Poly<
2 vs . . 3  setvar  s
3 vx . . 3  setvar  x
4 cc 9392 . . . 4  class  CC
54cpw 3969 . . 3  class  ~P CC
6 cn0 10691 . . 3  class  NN0
7 vp . . . . . . 7  setvar  p
87cv 1369 . . . . . 6  class  p
9 c0p 21281 . . . . . 6  class  0p
108, 9wceq 1370 . . . . 5  wff  p  =  0p
11 cdgr 21789 . . . . . . 7  class deg
128, 11cfv 5527 . . . . . 6  class  (deg `  p )
133cv 1369 . . . . . 6  class  x
14 clt 9530 . . . . . 6  class  <
1512, 13, 14wbr 4401 . . . . 5  wff  (deg `  p )  <  x
1610, 15wo 368 . . . 4  wff  ( p  =  0p  \/  (deg `  p )  <  x )
172cv 1369 . . . . 5  class  s
18 cply 21786 . . . . 5  class Poly
1917, 18cfv 5527 . . . 4  class  (Poly `  s )
2016, 7, 19crab 2803 . . 3  class  { p  e.  (Poly `  s )  |  ( p  =  0p  \/  (deg `  p )  <  x
) }
212, 3, 5, 6, 20cmpt2 6203 . 2  class  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0p  \/  (deg `  p )  <  x
) } )
221, 21wceq 1370 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