plyss - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > plyss		Structured version Visualization version GIF version

Theorem plyss 26102

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

**Assertion**
Ref	Expression
plyss	⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))

Proof of Theorem plyss Dummy variables 𝑘 𝑎 𝑛 𝑧 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 484	. . . . . . . 8 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → 𝑇 ⊆ ℂ)
2		cnex 11090	. . . . . . . 8 ⊢ ℂ ∈ V
3		ssexg 5262	. . . . . . . 8 ⊢ ((𝑇 ⊆ ℂ ∧ ℂ ∈ V) → 𝑇 ∈ V)
4	1, 2, 3	sylancl 586	. . . . . . 7 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → 𝑇 ∈ V)
5		snex 5375	. . . . . . 7 ⊢ {0} ∈ V
6		unexg 7679	. . . . . . 7 ⊢ ((𝑇 ∈ V ∧ {0} ∈ V) → (𝑇 ∪ {0}) ∈ V)
7	4, 5, 6	sylancl 586	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑇 ∪ {0}) ∈ V)
8		unss1 4136	. . . . . . 7 ⊢ (𝑆 ⊆ 𝑇 → (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0}))
9	8	adantr 480	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0}))
10		mapss 8816	. . . . . 6 ⊢ (((𝑇 ∪ {0}) ∈ V ∧ (𝑆 ∪ {0}) ⊆ (𝑇 ∪ {0})) → ((𝑆 ∪ {0}) ↑_m ℕ₀) ⊆ ((𝑇 ∪ {0}) ↑_m ℕ₀))
11	7, 9, 10	syl2anc 584	. . . . 5 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → ((𝑆 ∪ {0}) ↑_m ℕ₀) ⊆ ((𝑇 ∪ {0}) ↑_m ℕ₀))
12		ssrexv 4005	. . . . 5 ⊢ (((𝑆 ∪ {0}) ↑_m ℕ₀) ⊆ ((𝑇 ∪ {0}) ↑_m ℕ₀) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
13	11, 12	syl 17	. . . 4 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
14	13	reximdv 3144	. . 3 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘))) → ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))))
15	14	ss2abdv 4018	. 2 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))} ⊆ {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
16		sstr 3944	. . 3 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → 𝑆 ⊆ ℂ)
17		plyval 26096	. . 3 ⊢ (𝑆 ⊆ ℂ → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
18	16, 17	syl 17	. 2 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) = {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑆 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
19		plyval 26096	. . 3 ⊢ (𝑇 ⊆ ℂ → (Poly‘𝑇) = {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
20	19	adantl 481	. 2 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑇) = {𝑓 ∣ ∃𝑛 ∈ ℕ₀ ∃𝑎 ∈ ((𝑇 ∪ {0}) ↑_m ℕ₀)𝑓 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑛)((𝑎‘𝑘) · (𝑧↑𝑘)))})
21	15, 18, 20	3sstr4d 3991	1 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ⊆ ℂ) → (Poly‘𝑆) ⊆ (Poly‘𝑇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2109 {cab 2707 ∃wrex 3053 Vcvv 3436 ∪ cun 3901 ⊆ wss 3903 {csn 4577 ↦ cmpt 5173 ‘cfv 6482 (class class class)co 7349 ↑_m cmap 8753 ℂcc 11007 0cc0 11009 · cmul 11014 ℕ₀cn0 12384 ...cfz 13410 ↑cexp 13968 Σcsu 15593 Polycply 26087

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-1cn 11067 ax-addcl 11069

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-ral 3045 df-rex 3054 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-map 8755 df-nn 12129 df-n0 12385 df-ply 26091

This theorem is referenced by: plyssc 26103 elqaa 26228 aacjcl 26233 aalioulem3 26240 itgoss 43146 cnsrplycl 43150

W3C validator