![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ulmcl | Structured version Visualization version GIF version |
Description: Closure of a uniform limit of functions. (Contributed by Mario Carneiro, 26-Feb-2015.) |
Ref | Expression |
---|---|
ulmcl | ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ulmscl 24471 | . . . 4 ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝑆 ∈ V) | |
2 | ulmval 24472 | . . . 4 ⊢ (𝑆 ∈ V → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) | |
3 | 1, 2 | syl 17 | . . 3 ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → (𝐹(⇝𝑢‘𝑆)𝐺 ↔ ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥))) |
4 | 3 | ibi 259 | . 2 ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → ∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥)) |
5 | simp2 1168 | . . 3 ⊢ ((𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) → 𝐺:𝑆⟶ℂ) | |
6 | 5 | rexlimivw 3208 | . 2 ⊢ (∃𝑛 ∈ ℤ (𝐹:(ℤ≥‘𝑛)⟶(ℂ ↑𝑚 𝑆) ∧ 𝐺:𝑆⟶ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ (ℤ≥‘𝑛)∀𝑘 ∈ (ℤ≥‘𝑗)∀𝑧 ∈ 𝑆 (abs‘(((𝐹‘𝑘)‘𝑧) − (𝐺‘𝑧))) < 𝑥) → 𝐺:𝑆⟶ℂ) |
7 | 4, 6 | syl 17 | 1 ⊢ (𝐹(⇝𝑢‘𝑆)𝐺 → 𝐺:𝑆⟶ℂ) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ w3a 1108 ∈ wcel 2157 ∀wral 3087 ∃wrex 3088 Vcvv 3383 class class class wbr 4841 ⟶wf 6095 ‘cfv 6099 (class class class)co 6876 ↑𝑚 cmap 8093 ℂcc 10220 < clt 10361 − cmin 10554 ℤcz 11662 ℤ≥cuz 11926 ℝ+crp 12070 abscabs 14312 ⇝𝑢culm 24468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-cnex 10278 ax-resscn 10279 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-rex 3093 df-reu 3094 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-op 4373 df-uni 4627 df-iun 4710 df-br 4842 df-opab 4904 df-mpt 4921 df-id 5218 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-map 8095 df-pm 8096 df-neg 10557 df-z 11663 df-uz 11927 df-ulm 24469 |
This theorem is referenced by: ulmi 24478 ulmclm 24479 ulmres 24480 ulmshftlem 24481 ulmuni 24484 ulmcau 24487 ulmss 24489 ulmbdd 24490 ulmcn 24491 ulmdvlem1 24492 ulmdvlem3 24494 ulmdv 24495 mbfulm 24498 iblulm 24499 itgulm 24500 itgulm2 24501 pserulm 24514 lgamgulmlem6 25109 lgamgulm2 25111 knoppcnlem9 32991 |
Copyright terms: Public domain | W3C validator |