tgioo2 - Metamath Proof Explorer

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

Theorem tgioo2 22819

Description: The standard topology on the reals is a subspace of the complex metric topology. (Contributed by Mario Carneiro, 13-Aug-2014.)

**Hypothesis**
Ref	Expression
tgioo2.1	⊢ 𝐽 = (TopOpen‘ℂ_fld)

**Assertion**
Ref	Expression
tgioo2	⊢ (topGen‘ran (,)) = (𝐽 ↾_t ℝ)

**Proof of Theorem tgioo2**
Step	Hyp	Ref	Expression
1		eqid 2806	. 2 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
2		cnxmet 22789	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
3		ax-resscn 10278	. . 3 ⊢ ℝ ⊆ ℂ
4		tgioo2.1	. . . . 5 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
5	4	cnfldtopn 22798	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
6		eqid 2806	. . . 4 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7	1, 5, 6	metrest 22542	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ ℝ ⊆ ℂ) → (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))))
8	2, 3, 7	mp2an 675	. 2 ⊢ (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
9	1, 8	tgioo 22812	1 ⊢ (topGen‘ran (,)) = (𝐽 ↾_t ℝ)

Colors of variables: wff setvar class

Syntax hints: = wceq 1637 ∈ wcel 2156 ⊆ wss 3769 × cxp 5309 ran crn 5312 ↾ cres 5313 ∘ ccom 5315 ‘cfv 6101 (class class class)co 6874 ℂcc 10219 ℝcr 10220 − cmin 10551 (,)cioo 12393 abscabs 14197 ↾_t crest 16286 TopOpenctopn 16287 topGenctg 16303 ∞Metcxmt 19939 MetOpencmopn 19944 ℂ_fldccnfld 19954

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1877 ax-4 1894 ax-5 2001 ax-6 2068 ax-7 2104 ax-8 2158 ax-9 2165 ax-10 2185 ax-11 2201 ax-12 2214 ax-13 2420 ax-ext 2784 ax-rep 4964 ax-sep 4975 ax-nul 4983 ax-pow 5035 ax-pr 5096 ax-un 7179 ax-cnex 10277 ax-resscn 10278 ax-1cn 10279 ax-icn 10280 ax-addcl 10281 ax-addrcl 10282 ax-mulcl 10283 ax-mulrcl 10284 ax-mulcom 10285 ax-addass 10286 ax-mulass 10287 ax-distr 10288 ax-i2m1 10289 ax-1ne0 10290 ax-1rid 10291 ax-rnegex 10292 ax-rrecex 10293 ax-cnre 10294 ax-pre-lttri 10295 ax-pre-lttrn 10296 ax-pre-ltadd 10297 ax-pre-mulgt0 10298 ax-pre-sup 10299

This theorem depends on definitions: df-bi 198 df-an 385 df-or 866 df-3or 1101 df-3an 1102 df-tru 1641 df-ex 1860 df-nf 1864 df-sb 2061 df-eu 2634 df-mo 2635 df-clab 2793 df-cleq 2799 df-clel 2802 df-nfc 2937 df-ne 2979 df-nel 3082 df-ral 3101 df-rex 3102 df-reu 3103 df-rmo 3104 df-rab 3105 df-v 3393 df-sbc 3634 df-csb 3729 df-dif 3772 df-un 3774 df-in 3776 df-ss 3783 df-pss 3785 df-nul 4117 df-if 4280 df-pw 4353 df-sn 4371 df-pr 4373 df-tp 4375 df-op 4377 df-uni 4631 df-int 4670 df-iun 4714 df-br 4845 df-opab 4907 df-mpt 4924 df-tr 4947 df-id 5219 df-eprel 5224 df-po 5232 df-so 5233 df-fr 5270 df-we 5272 df-xp 5317 df-rel 5318 df-cnv 5319 df-co 5320 df-dm 5321 df-rn 5322 df-res 5323 df-ima 5324 df-pred 5893 df-ord 5939 df-on 5940 df-lim 5941 df-suc 5942 df-iota 6064 df-fun 6103 df-fn 6104 df-f 6105 df-f1 6106 df-fo 6107 df-f1o 6108 df-fv 6109 df-riota 6835 df-ov 6877 df-oprab 6878 df-mpt2 6879 df-om 7296 df-1st 7398 df-2nd 7399 df-wrecs 7642 df-recs 7704 df-rdg 7742 df-1o 7796 df-oadd 7800 df-er 7979 df-map 8094 df-en 8193 df-dom 8194 df-sdom 8195 df-fin 8196 df-sup 8587 df-inf 8588 df-pnf 10361 df-mnf 10362 df-xr 10363 df-ltxr 10364 df-le 10365 df-sub 10553 df-neg 10554 df-div 10970 df-nn 11306 df-2 11364 df-3 11365 df-4 11366 df-5 11367 df-6 11368 df-7 11369 df-8 11370 df-9 11371 df-n0 11560 df-z 11644 df-dec 11760 df-uz 11905 df-q 12008 df-rp 12047 df-xneg 12162 df-xadd 12163 df-xmul 12164 df-ioo 12397 df-fz 12550 df-seq 13025 df-exp 13084 df-cj 14062 df-re 14063 df-im 14064 df-sqrt 14198 df-abs 14199 df-struct 16070 df-ndx 16071 df-slot 16072 df-base 16074 df-plusg 16166 df-mulr 16167 df-starv 16168 df-tset 16172 df-ple 16173 df-ds 16175 df-unif 16176 df-rest 16288 df-topn 16289 df-topgen 16309 df-psmet 19946 df-xmet 19947 df-met 19948 df-bl 19949 df-mopn 19950 df-cnfld 19955 df-top 20912 df-topon 20929 df-bases 20964

This theorem is referenced by: rerest 22820 tgioo3 22821 zcld2 22831 metdcn 22856 ngnmcncn 22861 metdscn2 22873 abscncfALT 22936 cnrehmeo 22965 rellycmp 22969 evth 22971 evth2 22972 lebnumlem2 22974 resscdrg 23366 retopn 23379 cncombf 23639 cnmbf 23640 dvcjbr 23926 rolle 23967 cmvth 23968 mvth 23969 dvlip 23970 dvlipcn 23971 dvlip2 23972 c1liplem1 23973 dvgt0lem1 23979 dvle 23984 dvivthlem1 23985 dvne0 23988 lhop1lem 23990 lhop2 23992 lhop 23993 dvcnvrelem1 23994 dvcnvrelem2 23995 dvcnvre 23996 dvcvx 23997 dvfsumle 23998 dvfsumabs 24000 dvfsumlem2 24004 ftc1 24019 ftc1cn 24020 ftc2 24021 ftc2ditglem 24022 itgparts 24024 itgsubstlem 24025 taylthlem2 24342 efcvx 24417 pige3 24484 dvloglem 24608 logdmopn 24609 advlog 24614 advlogexp 24615 logccv 24623 loglesqrt 24713 lgamgulmlem2 24970 ftalem3 25015 log2sumbnd 25447 nmcnc 27879 ipasslem7 28019 rmulccn 30299 raddcn 30300 ftc2re 31001 knoppcnlem10 32809 knoppcnlem11 32810 broucube 33756 ftc1cnnc 33796 ftc2nc 33806 dvasin 33808 dvacos 33809 dvreasin 33810 dvreacos 33811 areacirclem1 33812 areacirc 33817 itgpowd 38300 lhe4.4ex1a 39028 refsumcn 39683 xrtgcntopre 40188 tgioo4 40280 climreeq 40325 limcresiooub 40354 limcresioolb 40355 lptioo2cn 40357 lptioo1cn 40358 limclner 40363 cncfiooicclem1 40586 jumpncnp 40591 dvmptresicc 40614 dvresioo 40616 dvbdfbdioolem1 40623 itgsin0pilem1 40645 itgsinexplem1 40649 itgcoscmulx 40664 itgsubsticclem 40670 itgiccshift 40675 itgperiod 40676 itgsbtaddcnst 40677 dirkeritg 40798 dirkercncflem2 40800 dirkercncflem3 40801 dirkercncflem4 40802 dirkercncf 40803 fourierdlem28 40831 fourierdlem32 40835 fourierdlem33 40836 fourierdlem39 40842 fourierdlem56 40858 fourierdlem57 40859 fourierdlem58 40860 fourierdlem59 40861 fourierdlem60 40862 fourierdlem61 40863 fourierdlem62 40864 fourierdlem68 40870 fourierdlem72 40874 fourierdlem73 40875 fourierdlem74 40876 fourierdlem75 40877 fourierdlem80 40882 fourierdlem94 40896 fourierdlem103 40905 fourierdlem104 40906 fourierdlem113 40915 fouriercnp 40922 fouriersw 40927 fouriercn 40928 etransclem2 40932 etransclem23 40953 etransclem35 40965 etransclem38 40968 etransclem39 40969 etransclem44 40974 etransclem45 40975 etransclem46 40976 etransclem47 40977

W3C validator