![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > limccl | Structured version Visualization version GIF version |
Description: Closure of the limit operator. (Contributed by Mario Carneiro, 25-Dec-2016.) |
Ref | Expression |
---|---|
limccl | ⊢ (𝐹 limℂ 𝐵) ⊆ ℂ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | limcrcl 25889 | . . . . 5 ⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ)) | |
2 | eqid 2726 | . . . . . 6 ⊢ ((TopOpen‘ℂfld) ↾t (dom 𝐹 ∪ {𝐵})) = ((TopOpen‘ℂfld) ↾t (dom 𝐹 ∪ {𝐵})) | |
3 | eqid 2726 | . . . . . 6 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld) | |
4 | 2, 3 | limcfval 25887 | . . . . 5 ⊢ ((𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℂ ∧ 𝐵 ∈ ℂ) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (dom 𝐹 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((((TopOpen‘ℂfld) ↾t (dom 𝐹 ∪ {𝐵})) CnP (TopOpen‘ℂfld))‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
5 | 1, 4 | syl 17 | . . . 4 ⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → ((𝐹 limℂ 𝐵) = {𝑦 ∣ (𝑧 ∈ (dom 𝐹 ∪ {𝐵}) ↦ if(𝑧 = 𝐵, 𝑦, (𝐹‘𝑧))) ∈ ((((TopOpen‘ℂfld) ↾t (dom 𝐹 ∪ {𝐵})) CnP (TopOpen‘ℂfld))‘𝐵)} ∧ (𝐹 limℂ 𝐵) ⊆ ℂ)) |
6 | 5 | simprd 494 | . . 3 ⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → (𝐹 limℂ 𝐵) ⊆ ℂ) |
7 | id 22 | . . 3 ⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝑥 ∈ (𝐹 limℂ 𝐵)) | |
8 | 6, 7 | sseldd 3980 | . 2 ⊢ (𝑥 ∈ (𝐹 limℂ 𝐵) → 𝑥 ∈ ℂ) |
9 | 8 | ssriv 3983 | 1 ⊢ (𝐹 limℂ 𝐵) ⊆ ℂ |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 {cab 2703 ∪ cun 3945 ⊆ wss 3947 ifcif 4524 {csn 4624 ↦ cmpt 5227 dom cdm 5673 ⟶wf 6540 ‘cfv 6544 (class class class)co 7414 ℂcc 11145 ↾t crest 17428 TopOpenctopn 17429 ℂfldccnfld 21337 CnP ccnp 23215 limℂ climc 25877 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7736 ax-cnex 11203 ax-resscn 11204 ax-1cn 11205 ax-icn 11206 ax-addcl 11207 ax-addrcl 11208 ax-mulcl 11209 ax-mulrcl 11210 ax-mulcom 11211 ax-addass 11212 ax-mulass 11213 ax-distr 11214 ax-i2m1 11215 ax-1ne0 11216 ax-1rid 11217 ax-rnegex 11218 ax-rrecex 11219 ax-cnre 11220 ax-pre-lttri 11221 ax-pre-lttrn 11222 ax-pre-ltadd 11223 ax-pre-mulgt0 11224 ax-pre-sup 11225 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3365 df-reu 3366 df-rab 3421 df-v 3465 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4324 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4907 df-int 4948 df-iun 4996 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6303 df-ord 6369 df-on 6370 df-lim 6371 df-suc 6372 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7867 df-1st 7993 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-rdg 8430 df-1o 8486 df-er 8724 df-map 8847 df-pm 8848 df-en 8965 df-dom 8966 df-sdom 8967 df-fin 8968 df-fi 9445 df-sup 9476 df-inf 9477 df-pnf 11289 df-mnf 11290 df-xr 11291 df-ltxr 11292 df-le 11293 df-sub 11485 df-neg 11486 df-div 11911 df-nn 12257 df-2 12319 df-3 12320 df-4 12321 df-5 12322 df-6 12323 df-7 12324 df-8 12325 df-9 12326 df-n0 12517 df-z 12603 df-dec 12722 df-uz 12867 df-q 12977 df-rp 13021 df-xneg 13138 df-xadd 13139 df-xmul 13140 df-fz 13531 df-seq 14014 df-exp 14074 df-cj 15097 df-re 15098 df-im 15099 df-sqrt 15233 df-abs 15234 df-struct 17142 df-slot 17177 df-ndx 17189 df-base 17207 df-plusg 17272 df-mulr 17273 df-starv 17274 df-tset 17278 df-ple 17279 df-ds 17281 df-unif 17282 df-rest 17430 df-topn 17431 df-topgen 17451 df-psmet 21329 df-xmet 21330 df-met 21331 df-bl 21332 df-mopn 21333 df-cnfld 21338 df-top 22882 df-topon 22899 df-topsp 22921 df-bases 22935 df-cnp 23218 df-xms 24312 df-ms 24313 df-limc 25881 |
This theorem is referenced by: ellimc2 25892 limcres 25901 limcco 25908 limciun 25909 limcun 25910 dvfval 25912 dvcl 25914 lhop1lem 26032 mullimc 45271 limcdm0 45273 limccog 45275 mullimcf 45278 limcperiod 45283 limcrecl 45284 limcleqr 45299 neglimc 45302 addlimc 45303 limclner 45306 sublimc 45307 reclimc 45308 divlimc 45311 cncfiooicclem1 45548 cncfiooicc 45549 itgioocnicc 45632 iblcncfioo 45633 fourierdlem60 45821 fourierdlem61 45822 fourierdlem73 45834 fourierdlem74 45835 fourierdlem75 45836 fourierdlem81 45842 fourierdlem103 45864 fourierdlem104 45865 fourierdlem112 45873 |
Copyright terms: Public domain | W3C validator |