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

Definition df-plylt 41866
Description: Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014.)
Assertion
Ref Expression
df-plylt Poly< = (𝑠 ∈ 𝒫 β„‚, π‘₯ ∈ β„•0 ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)})
Distinct variable group:   𝑠,𝑝,π‘₯

Detailed syntax breakdown of Definition df-plylt
StepHypRef Expression
1 cplylt 41864 . 2 class Poly<
2 vs . . 3 setvar 𝑠
3 vx . . 3 setvar π‘₯
4 cc 11107 . . . 4 class β„‚
54cpw 4602 . . 3 class 𝒫 β„‚
6 cn0 12471 . . 3 class β„•0
7 vp . . . . . . 7 setvar 𝑝
87cv 1540 . . . . . 6 class 𝑝
9 c0p 25185 . . . . . 6 class 0𝑝
108, 9wceq 1541 . . . . 5 wff 𝑝 = 0𝑝
11 cdgr 25700 . . . . . . 7 class deg
128, 11cfv 6543 . . . . . 6 class (degβ€˜π‘)
133cv 1540 . . . . . 6 class π‘₯
14 clt 11247 . . . . . 6 class <
1512, 13, 14wbr 5148 . . . . 5 wff (degβ€˜π‘) < π‘₯
1610, 15wo 845 . . . 4 wff (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)
172cv 1540 . . . . 5 class 𝑠
18 cply 25697 . . . . 5 class Poly
1917, 18cfv 6543 . . . 4 class (Polyβ€˜π‘ )
2016, 7, 19crab 3432 . . 3 class {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)}
212, 3, 5, 6, 20cmpo 7410 . 2 class (𝑠 ∈ 𝒫 β„‚, π‘₯ ∈ β„•0 ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)})
221, 21wceq 1541 1 wff Poly< = (𝑠 ∈ 𝒫 β„‚, π‘₯ ∈ β„•0 ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator