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< = ( 𝑠 ∈ 𝒫 ℂ , 𝑥 ∈ ℕ0 ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( 𝑝 = 0𝑝 ∨ ( deg ‘ 𝑝 ) < 𝑥 ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cplylt	⊢ Poly<
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3	2	cpw	⊢ 𝒫 ℂ
4		vx	⊢ 𝑥
5		cn0	⊢ ℕ0
6		vp	⊢ 𝑝
7		cply	⊢ Poly
8	1	cv	⊢ 𝑠
9	8 7	cfv	⊢ ( Poly ‘ 𝑠 )
10	6	cv	⊢ 𝑝
11		c0p	⊢ 0𝑝
12	10 11	wceq	⊢ 𝑝 = 0𝑝
13		cdgr	⊢ deg
14	10 13	cfv	⊢ ( deg ‘ 𝑝 )
15		clt	⊢ <
16	4	cv	⊢ 𝑥
17	14 16 15	wbr	⊢ ( deg ‘ 𝑝 ) < 𝑥
18	12 17	wo	⊢ ( 𝑝 = 0𝑝 ∨ ( deg ‘ 𝑝 ) < 𝑥 )
19	18 6 9	crab	⊢ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( 𝑝 = 0𝑝 ∨ ( deg ‘ 𝑝 ) < 𝑥 ) }
20	1 4 3 5 19	cmpo	⊢ ( 𝑠 ∈ 𝒫 ℂ , 𝑥 ∈ ℕ0 ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( 𝑝 = 0𝑝 ∨ ( deg ‘ 𝑝 ) < 𝑥 ) } )
21	0 20	wceq	⊢ Poly< = ( 𝑠 ∈ 𝒫 ℂ , 𝑥 ∈ ℕ0 ↦ { 𝑝 ∈ ( Poly ‘ 𝑠 ) ∣ ( 𝑝 = 0𝑝 ∨ ( deg ‘ 𝑝 ) < 𝑥 ) } )