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\in \mathrm{Poly}\left(S\right)\to S\subseteq ℂ$$

Proof

Step	Hyp	Ref	Expression
1		df-ply	$$⊢\mathrm{Poly}=\left(x\in 𝒫ℂ⟼\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\right)$$
2	1	mptrcl	$$⊢F\in \mathrm{Poly}\left(S\right)\to S\in 𝒫ℂ$$
3	2	elpwid	$$⊢F\in \mathrm{Poly}\left(S\right)\to S\subseteq ℂ$$