Metamath Proof Explorer

Theorem plybss

Description: Reverse closure of the parameter S of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Assertion plybss F Poly S S


Step Hyp Ref Expression
1 df-ply Poly = x 𝒫 f | n 0 a x 0 0 f = z k = 0 n a k z k
2 1 mptrcl F Poly S S 𝒫
3 2 elpwid F Poly S S