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 40948
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 40946 . 2 class Poly<
2 vs . . 3 setvar 𝑠
3 vx . . 3 setvar 𝑥
4 cc 10862 . . . 4 class
54cpw 4539 . . 3 class 𝒫 ℂ
6 cn0 12225 . . 3 class 0
7 vp . . . . . . 7 setvar 𝑝
87cv 1541 . . . . . 6 class 𝑝
9 c0p 24823 . . . . . 6 class 0𝑝
108, 9wceq 1542 . . . . 5 wff 𝑝 = 0𝑝
11 cdgr 25338 . . . . . . 7 class deg
128, 11cfv 6431 . . . . . 6 class (deg‘𝑝)
133cv 1541 . . . . . 6 class 𝑥
14 clt 11002 . . . . . 6 class <
1512, 13, 14wbr 5079 . . . . 5 wff (deg‘𝑝) < 𝑥
1610, 15wo 844 . . . 4 wff (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)
172cv 1541 . . . . 5 class 𝑠
18 cply 25335 . . . . 5 class Poly
1917, 18cfv 6431 . . . 4 class (Poly‘𝑠)
2016, 7, 19crab 3070 . . 3 class {𝑝 ∈ (Poly‘𝑠) ∣ (𝑝 = 0𝑝 ∨ (deg‘𝑝) < 𝑥)}
212, 3, 5, 6, 20cmpo 7271 . 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