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

Definition df-plylt 27338
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  =  0 p  \/  (deg `  p )  <  x
) } )
Distinct variable group:    s, p, x

Detailed syntax breakdown of Definition df-plylt
StepHypRef Expression
1 cplylt 27336 . 2  class Poly<
2 vs . . 3  set  s
3 vx . . 3  set  x
4 cc 8735 . . . 4  class  CC
54cpw 3625 . . 3  class  ~P CC
6 cn0 9965 . . 3  class  NN0
7 vp . . . . . . 7  set  p
87cv 1622 . . . . . 6  class  p
9 c0p 19024 . . . . . 6  class  0 p
108, 9wceq 1623 . . . . 5  wff  p  =  0 p
11 cdgr 19569 . . . . . . 7  class deg
128, 11cfv 5255 . . . . . 6  class  (deg `  p )
133cv 1622 . . . . . 6  class  x
14 clt 8867 . . . . . 6  class  <
1512, 13, 14wbr 4023 . . . . 5  wff  (deg `  p )  <  x
1610, 15wo 357 . . . 4  wff  ( p  =  0 p  \/  (deg `  p )  < 
x )
172cv 1622 . . . . 5  class  s
18 cply 19566 . . . . 5  class Poly
1917, 18cfv 5255 . . . 4  class  (Poly `  s )
2016, 7, 19crab 2547 . . 3  class  { p  e.  (Poly `  s )  |  ( p  =  0 p  \/  (deg `  p )  <  x
) }
212, 3, 5, 6, 20cmpt2 5860 . 2  class  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0 p  \/  (deg `  p )  <  x
) } )
221, 21wceq 1623 1  wff Poly<  =  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0 p  \/  (deg `  p )  <  x
) } )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator