Metamath Proof Explorer


Definition df-plylt

Description: Define the class of limited-degree polynomials. (Contributed by Stefan O'Rear, 8-Dec-2014)

Ref Expression
Assertion df-plylt Poly < = s 𝒫 , x 0 p Poly s | p = 0 𝑝 deg p < x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cplylt class Poly <
1 vs setvar s
2 cc class
3 2 cpw class 𝒫
4 vx setvar x
5 cn0 class 0
6 vp setvar p
7 cply class Poly
8 1 cv setvar s
9 8 7 cfv class Poly s
10 6 cv setvar p
11 c0p class 0 𝑝
12 10 11 wceq wff p = 0 𝑝
13 cdgr class deg
14 10 13 cfv class deg p
15 clt class <
16 4 cv setvar x
17 14 16 15 wbr wff deg p < x
18 12 17 wo wff p = 0 𝑝 deg p < x
19 18 6 9 crab class p Poly s | p = 0 𝑝 deg p < x
20 1 4 3 5 19 cmpo class s 𝒫 , x 0 p Poly s | p = 0 𝑝 deg p < x
21 0 20 wceq wff Poly < = s 𝒫 , x 0 p Poly s | p = 0 𝑝 deg p < x