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 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
13 11 12 syl ⊢ S ⊆ T ∧ T ⊆ ℂ → ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
14 13 reximdv ⊢ S ⊆ T ∧ T ⊆ ℂ → ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k → ∃ n ∈ ℕ 0 ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
15 14 ss2abdv ⊢ S ⊆ T ∧ T ⊆ ℂ → f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k ⊆ f | ∃ n ∈ ℕ 0 ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
16 sstr ⊢ S ⊆ T ∧ T ⊆ ℂ → S ⊆ ℂ
17 plyval ⊢ S ⊆ ℂ → Poly ⁡ S = f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
18 16 17 syl ⊢ S ⊆ T ∧ T ⊆ ℂ → Poly ⁡ S = f | ∃ n ∈ ℕ 0 ∃ a ∈ S ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
19 plyval ⊢ T ⊆ ℂ → Poly ⁡ T = f | ∃ n ∈ ℕ 0 ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
20 19 adantl ⊢ S ⊆ T ∧ T ⊆ ℂ → Poly ⁡ T = f | ∃ n ∈ ℕ 0 ∃ a ∈ T ∪ 0 ℕ 0 f = z ∈ ℂ ⟼ ∑ k = 0 n a ⁡ k ⁢ z k
21 15 18 20 3sstr4d ⊢ S ⊆ T ∧ T ⊆ ℂ → Poly ⁡ S ⊆ Poly ⁡ T