Description: Reverse closure of the parameter S of the polynomial set function. (Contributed by Mario Carneiro, 22-Jul-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | plybss | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ply | ⊢ Poly = ( 𝑥 ∈ 𝒫 ℂ ↦ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ_{0} ∃ 𝑎 ∈ ( ( 𝑥 ∪ { 0 } ) ↑_{m} ℕ_{0} ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } ) | |
2 | 1 | mptrcl | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ∈ 𝒫 ℂ ) |
3 | 2 | elpwid | ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑆 ⊆ ℂ ) |