This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑇 ⊆ ℂ )
2 cnex ⊢ ℂ ∈ V
3 ssexg ⊢ ( ( 𝑇 ⊆ ℂ ∧ ℂ ∈ V ) → 𝑇 ∈ V )
4 1 2 3 sylancl ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑇 ∈ V )
5 snex ⊢ { 0 } ∈ V
6 unexg ⊢ ( ( 𝑇 ∈ V ∧ { 0 } ∈ V ) → ( 𝑇 ∪ { 0 } ) ∈ V )
7 4 5 6 sylancl ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑇 ∪ { 0 } ) ∈ V )
8 unss1 ⊢ ( 𝑆 ⊆ 𝑇 → ( 𝑆 ∪ { 0 } ) ⊆ ( 𝑇 ∪ { 0 } ) )
9 8 adantr ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( 𝑆 ∪ { 0 } ) ⊆ ( 𝑇 ∪ { 0 } ) )
10 mapss ⊢ ( ( ( 𝑇 ∪ { 0 } ) ∈ V ∧ ( 𝑆 ∪ { 0 } ) ⊆ ( 𝑇 ∪ { 0 } ) ) → ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ⊆ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) )
11 7 9 10 syl2anc ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ⊆ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) )
12 ssrexv ⊢ ( ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ⊆ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
13 11 12 syl ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
14 13 reximdv ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) → ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) ) )
15 14 ss2abdv ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } ⊆ { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
16 sstr ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → 𝑆 ⊆ ℂ )
17 plyval ⊢ ( 𝑆 ⊆ ℂ → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
18 16 17 syl ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( Poly ‘ 𝑆 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
19 plyval ⊢ ( 𝑇 ⊆ ℂ → ( Poly ‘ 𝑇 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
20 19 adantl ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( Poly ‘ 𝑇 ) = { 𝑓 ∣ ∃ 𝑛 ∈ ℕ0 ∃ 𝑎 ∈ ( ( 𝑇 ∪ { 0 } ) ↑m ℕ0 ) 𝑓 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑎 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) } )
21 15 18 20 3sstr4d ⊢ ( ( 𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ ) → ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ 𝑇 ) )