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 ⊢S⊆T∧T⊆ℂ→Poly⁡S⊆Poly⁡T

Proof

Step Hyp Ref Expression
1 simpr ⊢S⊆T∧T⊆ℂ→T⊆ℂ
2 cnex ⊢ℂ∈V
3 ssexg ⊢T⊆ℂ∧ℂ∈V→T∈V
4 1 2 3 sylancl ⊢S⊆T∧T⊆ℂ→T∈V
5 snex ⊢0∈V
6 unexg ⊢T∈V∧0∈V→T∪0∈V
7 4 5 6 sylancl ⊢S⊆T∧T⊆ℂ→T∪0∈V
8 unss1 ⊢S⊆T→S∪0⊆T∪0
9 8 adantr ⊢S⊆T∧T⊆ℂ→S∪0⊆T∪0
10 mapss ⊢T∪0∈V∧S∪0⊆T∪0→S∪0ℕ0⊆T∪0ℕ0
11 7 9 10 syl2anc ⊢S⊆T∧T⊆ℂ→S∪0ℕ0⊆T∪0ℕ0
12 ssrexv ⊢S∪0ℕ0⊆T∪0ℕ0→∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk→∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
13 11 12 syl ⊢S⊆T∧T⊆ℂ→∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk→∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
14 13 reximdv ⊢S⊆T∧T⊆ℂ→∃n∈ℕ0∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk→∃n∈ℕ0∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
15 14 ss2abdv ⊢S⊆T∧T⊆ℂ→f|∃n∈ℕ0∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk⊆f|∃n∈ℕ0∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
16 sstr ⊢S⊆T∧T⊆ℂ→S⊆ℂ
17 plyval ⊢S⊆ℂ→Poly⁡S=f|∃n∈ℕ0∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
18 16 17 syl ⊢S⊆T∧T⊆ℂ→Poly⁡S=f|∃n∈ℕ0∃a∈S∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
19 plyval ⊢T⊆ℂ→Poly⁡T=f|∃n∈ℕ0∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
20 19 adantl ⊢S⊆T∧T⊆ℂ→Poly⁡T=f|∃n∈ℕ0∃a∈T∪0ℕ0f=z∈ℂ⟼∑k=0na⁡k⁢zk
21 15 18 20 3sstr4d ⊢S⊆T∧T⊆ℂ→Poly⁡S⊆Poly⁡T