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 27441
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 27439 . 2  class Poly<
2 vs . . 3  set  s
3 vx . . 3  set  x
4 cc 8751 . . . 4  class  CC
54cpw 3638 . . 3  class  ~P CC
6 cn0 9981 . . 3  class  NN0
7 vp . . . . . . 7  set  p
87cv 1631 . . . . . 6  class  p
9 c0p 19040 . . . . . 6  class  0 p
108, 9wceq 1632 . . . . 5  wff  p  =  0 p
11 cdgr 19585 . . . . . . 7  class deg
128, 11cfv 5271 . . . . . 6  class  (deg `  p )
133cv 1631 . . . . . 6  class  x
14 clt 8883 . . . . . 6  class  <
1512, 13, 14wbr 4039 . . . . 5  wff  (deg `  p )  <  x
1610, 15wo 357 . . . 4  wff  ( p  =  0 p  \/  (deg `  p )  < 
x )
172cv 1631 . . . . 5  class  s
18 cply 19582 . . . . 5  class Poly
1917, 18cfv 5271 . . . 4  class  (Poly `  s )
2016, 7, 19crab 2560 . . 3  class  { p  e.  (Poly `  s )  |  ( p  =  0 p  \/  (deg `  p )  <  x
) }
212, 3, 5, 6, 20cmpt2 5876 . 2  class  ( s  e.  ~P CC ,  x  e.  NN0  |->  { p  e.  (Poly `  s )  |  ( p  =  0 p  \/  (deg `  p )  <  x
) } )
221, 21wceq 1632 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