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 23094

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 2795	. 2 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
2		cnxmet 23064	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
3		ax-resscn 10440	. . 3 ⊢ ℝ ⊆ ℂ
4		tgioo2.1	. . . . 5 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
5	4	cnfldtopn 23073	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
6		eqid 2795	. . . 4 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7	1, 5, 6	metrest 22817	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ ℝ ⊆ ℂ) → (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))))
8	2, 3, 7	mp2an 688	. 2 ⊢ (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
9	1, 8	tgioo 23087	1 ⊢ (topGen‘ran (,)) = (𝐽 ↾_t ℝ)

Colors of variables: wff setvar class

Syntax hints: = wceq 1522 ∈ wcel 2081 ⊆ wss 3859 × cxp 5441 ran crn 5444 ↾ cres 5445 ∘ ccom 5447 ‘cfv 6225 (class class class)co 7016 ℂcc 10381 ℝcr 10382 − cmin 10717 (,)cioo 12588 abscabs 14427 ↾_t crest 16523 TopOpenctopn 16524 topGenctg 16540 ∞Metcxmet 20212 MetOpencmopn 20217 ℂ_fldccnfld 20227

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5081 ax-sep 5094 ax-nul 5101 ax-pow 5157 ax-pr 5221 ax-un 7319 ax-cnex 10439 ax-resscn 10440 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-mulcom 10447 ax-addass 10448 ax-mulass 10449 ax-distr 10450 ax-i2m1 10451 ax-1ne0 10452 ax-1rid 10453 ax-rnegex 10454 ax-rrecex 10455 ax-cnre 10456 ax-pre-lttri 10457 ax-pre-lttrn 10458 ax-pre-ltadd 10459 ax-pre-mulgt0 10460 ax-pre-sup 10461

This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-nel 3091 df-ral 3110 df-rex 3111 df-reu 3112 df-rmo 3113 df-rab 3114 df-v 3439 df-sbc 3707 df-csb 3812 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-pss 3876 df-nul 4212 df-if 4382 df-pw 4455 df-sn 4473 df-pr 4475 df-tp 4477 df-op 4479 df-uni 4746 df-int 4783 df-iun 4827 df-br 4963 df-opab 5025 df-mpt 5042 df-tr 5064 df-id 5348 df-eprel 5353 df-po 5362 df-so 5363 df-fr 5402 df-we 5404 df-xp 5449 df-rel 5450 df-cnv 5451 df-co 5452 df-dm 5453 df-rn 5454 df-res 5455 df-ima 5456 df-pred 6023 df-ord 6069 df-on 6070 df-lim 6071 df-suc 6072 df-iota 6189 df-fun 6227 df-fn 6228 df-f 6229 df-f1 6230 df-fo 6231 df-f1o 6232 df-fv 6233 df-riota 6977 df-ov 7019 df-oprab 7020 df-mpo 7021 df-om 7437 df-1st 7545 df-2nd 7546 df-wrecs 7798 df-recs 7860 df-rdg 7898 df-1o 7953 df-oadd 7957 df-er 8139 df-map 8258 df-en 8358 df-dom 8359 df-sdom 8360 df-fin 8361 df-sup 8752 df-inf 8753 df-pnf 10523 df-mnf 10524 df-xr 10525 df-ltxr 10526 df-le 10527 df-sub 10719 df-neg 10720 df-div 11146 df-nn 11487 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 df-7 11553 df-8 11554 df-9 11555 df-n0 11746 df-z 11830 df-dec 11948 df-uz 12094 df-q 12198 df-rp 12240 df-xneg 12357 df-xadd 12358 df-xmul 12359 df-ioo 12592 df-fz 12743 df-seq 13220 df-exp 13280 df-cj 14292 df-re 14293 df-im 14294 df-sqrt 14428 df-abs 14429 df-struct 16314 df-ndx 16315 df-slot 16316 df-base 16318 df-plusg 16407 df-mulr 16408 df-starv 16409 df-tset 16413 df-ple 16414 df-ds 16416 df-unif 16417 df-rest 16525 df-topn 16526 df-topgen 16546 df-psmet 20219 df-xmet 20220 df-met 20221 df-bl 20222 df-mopn 20223 df-cnfld 20228 df-top 21186 df-topon 21203 df-bases 21238

This theorem is referenced by: rerest 23095 tgioo3 23096 zcld2 23106 metdcn 23131 ngnmcncn 23136 metdscn2 23148 abscncfALT 23211 cnrehmeo 23240 rellycmp 23244 evth 23246 evth2 23247 lebnumlem2 23249 resscdrg 23644 retopn 23665 cncombf 23942 cnmbf 23943 dvcjbr 24229 rolle 24270 cmvth 24271 mvth 24272 dvlip 24273 dvlipcn 24274 dvlip2 24275 c1liplem1 24276 dvgt0lem1 24282 dvle 24287 dvivthlem1 24288 dvne0 24291 lhop1lem 24293 lhop2 24295 lhop 24296 dvcnvrelem1 24297 dvcnvrelem2 24298 dvcnvre 24299 dvcvx 24300 dvfsumle 24301 dvfsumabs 24303 dvfsumlem2 24307 ftc1 24322 ftc1cn 24323 ftc2 24324 ftc2ditglem 24325 itgparts 24327 itgsubstlem 24328 taylthlem2 24645 efcvx 24720 pige3ALT 24788 dvloglem 24912 logdmopn 24913 advlog 24918 advlogexp 24919 logccv 24927 loglesqrt 25020 lgamgulmlem2 25289 ftalem3 25334 log2sumbnd 25802 nmcnc 28164 ipasslem7 28304 rmulccn 30788 raddcn 30789 ftc2re 31486 knoppcnlem10 33450 knoppcnlem11 33451 broucube 34457 ftc1cnnc 34497 ftc2nc 34507 dvasin 34509 dvacos 34510 dvreasin 34511 dvreacos 34512 areacirclem1 34513 areacirc 34518 itgpowd 39306 lhe4.4ex1a 40199 refsumcn 40826 xrtgcntopre 41297 tgioo4 41391 climreeq 41436 limcresiooub 41465 limcresioolb 41466 lptioo2cn 41468 lptioo1cn 41469 limclner 41474 cncfiooicclem1 41717 jumpncnp 41722 dvmptresicc 41745 dvresioo 41747 dvbdfbdioolem1 41754 itgsin0pilem1 41776 itgsinexplem1 41780 itgcoscmulx 41795 itgsubsticclem 41801 itgiccshift 41806 itgperiod 41807 itgsbtaddcnst 41808 dirkeritg 41929 dirkercncflem2 41931 dirkercncflem3 41932 dirkercncflem4 41933 dirkercncf 41934 fourierdlem28 41962 fourierdlem32 41966 fourierdlem33 41967 fourierdlem39 41973 fourierdlem56 41989 fourierdlem57 41990 fourierdlem58 41991 fourierdlem59 41992 fourierdlem60 41993 fourierdlem61 41994 fourierdlem62 41995 fourierdlem68 42001 fourierdlem72 42005 fourierdlem73 42006 fourierdlem74 42007 fourierdlem75 42008 fourierdlem80 42013 fourierdlem94 42027 fourierdlem103 42036 fourierdlem104 42037 fourierdlem113 42046 fouriercnp 42053 fouriersw 42058 fouriercn 42059 etransclem2 42063 etransclem23 42084 etransclem35 42096 etransclem38 42099 etransclem39 42100 etransclem44 42105 etransclem45 42106 etransclem46 42107 etransclem47 42108

W3C validator