# Metamath Proof Explorer

## Theorem plyss

Description: The polynomial set function preserves the subset relation. (Contributed by Mario Carneiro, 17-Jul-2014)

Ref Expression
Assertion plyss ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left({T}\right)$

### Proof

Step Hyp Ref Expression
1 simpr ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {T}\subseteq ℂ$
2 cnex ${⊢}ℂ\in \mathrm{V}$
3 ssexg ${⊢}\left({T}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {T}\in \mathrm{V}$
4 1 2 3 sylancl ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {T}\in \mathrm{V}$
5 snex ${⊢}\left\{0\right\}\in \mathrm{V}$
6 unexg ${⊢}\left({T}\in \mathrm{V}\wedge \left\{0\right\}\in \mathrm{V}\right)\to {T}\cup \left\{0\right\}\in \mathrm{V}$
7 4 5 6 sylancl ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {T}\cup \left\{0\right\}\in \mathrm{V}$
8 unss1 ${⊢}{S}\subseteq {T}\to {S}\cup \left\{0\right\}\subseteq {T}\cup \left\{0\right\}$
9 8 adantr ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {S}\cup \left\{0\right\}\subseteq {T}\cup \left\{0\right\}$
10 mapss ${⊢}\left({T}\cup \left\{0\right\}\in \mathrm{V}\wedge {S}\cup \left\{0\right\}\subseteq {T}\cup \left\{0\right\}\right)\to {\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\subseteq {\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}$
11 7 9 10 syl2anc ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\subseteq {\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}$
12 ssrexv ${⊢}{\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\subseteq {\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\to \left(\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to \exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
13 11 12 syl ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left(\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to \exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
14 13 reximdv ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left(\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\to \exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right)$
15 14 ss2abdv ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}\subseteq \left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}$
16 sstr ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to {S}\subseteq ℂ$
17 plyval ${⊢}{S}\subseteq ℂ\to \mathrm{Poly}\left({S}\right)=\left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}$
18 16 17 syl ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \mathrm{Poly}\left({S}\right)=\left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}$
19 plyval ${⊢}{T}\subseteq ℂ\to \mathrm{Poly}\left({T}\right)=\left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}$
20 19 adantl ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \mathrm{Poly}\left({T}\right)=\left\{{f}|\exists {n}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\exists {a}\in \left({\left({T}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)\phantom{\rule{.4em}{0ex}}{f}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{n}}{a}\left({k}\right){{z}}^{{k}}\right)\right\}$
21 15 18 20 3sstr4d ${⊢}\left({S}\subseteq {T}\wedge {T}\subseteq ℂ\right)\to \mathrm{Poly}\left({S}\right)\subseteq \mathrm{Poly}\left({T}\right)$