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	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )

Proof

Step	Hyp	Ref	Expression
1		df-ply	⊢ Poly = ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
2	1	mptrcl	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ∈ 𝒫 ℂ )
3	2	elpwid	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ )