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 41490
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 41488 . 2 class Poly<
2 vs . . 3 setvar 𝑠
3 vx . . 3 setvar π‘₯
4 cc 11056 . . . 4 class β„‚
54cpw 4565 . . 3 class 𝒫 β„‚
6 cn0 12420 . . 3 class β„•0
7 vp . . . . . . 7 setvar 𝑝
87cv 1541 . . . . . 6 class 𝑝
9 c0p 25049 . . . . . 6 class 0𝑝
108, 9wceq 1542 . . . . 5 wff 𝑝 = 0𝑝
11 cdgr 25564 . . . . . . 7 class deg
128, 11cfv 6501 . . . . . 6 class (degβ€˜π‘)
133cv 1541 . . . . . 6 class π‘₯
14 clt 11196 . . . . . 6 class <
1512, 13, 14wbr 5110 . . . . 5 wff (degβ€˜π‘) < π‘₯
1610, 15wo 846 . . . 4 wff (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)
172cv 1541 . . . . 5 class 𝑠
18 cply 25561 . . . . 5 class Poly
1917, 18cfv 6501 . . . 4 class (Polyβ€˜π‘ )
2016, 7, 19crab 3410 . . 3 class {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)}
212, 3, 5, 6, 20cmpo 7364 . 2 class (𝑠 ∈ 𝒫 β„‚, π‘₯ ∈ β„•0 ↦ {𝑝 ∈ (Polyβ€˜π‘ ) ∣ (𝑝 = 0𝑝 ∨ (degβ€˜π‘) < π‘₯)})
221, 21wceq 1542 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