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 23975

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 2739	. 2 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
2		cnxmet 23945	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
3		ax-resscn 10937	. . 3 ⊢ ℝ ⊆ ℂ
4		tgioo2.1	. . . . 5 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
5	4	cnfldtopn 23954	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
6		eqid 2739	. . . 4 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7	1, 5, 6	metrest 23689	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ ℝ ⊆ ℂ) → (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))))
8	2, 3, 7	mp2an 689	. 2 ⊢ (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
9	1, 8	tgioo 23968	1 ⊢ (topGen‘ran (,)) = (𝐽 ↾_t ℝ)

Colors of variables: wff setvar class

Syntax hints: = wceq 1539 ∈ wcel 2107 ⊆ wss 3888 × cxp 5588 ran crn 5591 ↾ cres 5592 ∘ ccom 5594 ‘cfv 6437 (class class class)co 7284 ℂcc 10878 ℝcr 10879 − cmin 11214 (,)cioo 13088 abscabs 14954 ↾_t crest 17140 TopOpenctopn 17141 topGenctg 17157 ∞Metcxmet 20591 MetOpencmopn 20596 ℂ_fldccnfld 20606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2710 ax-rep 5210 ax-sep 5224 ax-nul 5231 ax-pow 5289 ax-pr 5353 ax-un 7597 ax-cnex 10936 ax-resscn 10937 ax-1cn 10938 ax-icn 10939 ax-addcl 10940 ax-addrcl 10941 ax-mulcl 10942 ax-mulrcl 10943 ax-mulcom 10944 ax-addass 10945 ax-mulass 10946 ax-distr 10947 ax-i2m1 10948 ax-1ne0 10949 ax-1rid 10950 ax-rnegex 10951 ax-rrecex 10952 ax-cnre 10953 ax-pre-lttri 10954 ax-pre-lttrn 10955 ax-pre-ltadd 10956 ax-pre-mulgt0 10957 ax-pre-sup 10958

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-nel 3051 df-ral 3070 df-rex 3071 df-rmo 3072 df-reu 3073 df-rab 3074 df-v 3435 df-sbc 3718 df-csb 3834 df-dif 3891 df-un 3893 df-in 3895 df-ss 3905 df-pss 3907 df-nul 4258 df-if 4461 df-pw 4536 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4841 df-iun 4927 df-br 5076 df-opab 5138 df-mpt 5159 df-tr 5193 df-id 5490 df-eprel 5496 df-po 5504 df-so 5505 df-fr 5545 df-we 5547 df-xp 5596 df-rel 5597 df-cnv 5598 df-co 5599 df-dm 5600 df-rn 5601 df-res 5602 df-ima 5603 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6395 df-fun 6439 df-fn 6440 df-f 6441 df-f1 6442 df-fo 6443 df-f1o 6444 df-fv 6445 df-riota 7241 df-ov 7287 df-oprab 7288 df-mpo 7289 df-om 7722 df-1st 7840 df-2nd 7841 df-frecs 8106 df-wrecs 8137 df-recs 8211 df-rdg 8250 df-1o 8306 df-er 8507 df-map 8626 df-en 8743 df-dom 8744 df-sdom 8745 df-fin 8746 df-sup 9210 df-inf 9211 df-pnf 11020 df-mnf 11021 df-xr 11022 df-ltxr 11023 df-le 11024 df-sub 11216 df-neg 11217 df-div 11642 df-nn 11983 df-2 12045 df-3 12046 df-4 12047 df-5 12048 df-6 12049 df-7 12050 df-8 12051 df-9 12052 df-n0 12243 df-z 12329 df-dec 12447 df-uz 12592 df-q 12698 df-rp 12740 df-xneg 12857 df-xadd 12858 df-xmul 12859 df-ioo 13092 df-fz 13249 df-seq 13731 df-exp 13792 df-cj 14819 df-re 14820 df-im 14821 df-sqrt 14955 df-abs 14956 df-struct 16857 df-slot 16892 df-ndx 16904 df-base 16922 df-plusg 16984 df-mulr 16985 df-starv 16986 df-tset 16990 df-ple 16991 df-ds 16993 df-unif 16994 df-rest 17142 df-topn 17143 df-topgen 17163 df-psmet 20598 df-xmet 20599 df-met 20600 df-bl 20601 df-mopn 20602 df-cnfld 20607 df-top 22052 df-topon 22069 df-bases 22105

This theorem is referenced by: rerest 23976 tgioo3 23977 zcld2 23987 metdcn 24012 ngnmcncn 24017 metdscn2 24029 abscncfALT 24096 cnrehmeo 24125 rellycmp 24129 evth 24131 evth2 24132 lebnumlem2 24134 resscdrg 24531 retopn 24552 cncombf 24831 cnmbf 24832 dvmptresicc 25089 dvcjbr 25122 rolle 25163 cmvth 25164 mvth 25165 dvlip 25166 dvlipcn 25167 dvlip2 25168 c1liplem1 25169 dvgt0lem1 25175 dvle 25180 dvivthlem1 25181 dvne0 25184 lhop1lem 25186 lhop2 25188 lhop 25189 dvcnvrelem1 25190 dvcnvrelem2 25191 dvcnvre 25192 dvcvx 25193 dvfsumle 25194 dvfsumabs 25196 dvfsumlem2 25200 ftc1 25215 ftc1cn 25216 ftc2 25217 ftc2ditglem 25218 itgparts 25220 itgsubstlem 25221 itgpowd 25223 taylthlem2 25542 efcvx 25617 pige3ALT 25685 dvloglem 25812 logdmopn 25813 advlog 25818 advlogexp 25819 logccv 25827 loglesqrt 25920 lgamgulmlem2 26188 ftalem3 26233 log2sumbnd 26701 nmcnc 29067 ipasslem7 29207 rmulccn 31887 raddcn 31888 ftc2re 32587 knoppcnlem10 34691 knoppcnlem11 34692 broucube 35820 ftc1cnnc 35858 ftc2nc 35868 dvasin 35870 dvacos 35871 dvreasin 35872 dvreacos 35873 areacirclem1 35874 areacirc 35879 dvrelog2 40079 dvrelog3 40080 aks4d1p1p6 40088 lhe4.4ex1a 41954 refsumcn 42580 xrtgcntopre 43026 tgioo4 43118 climreeq 43161 limcresiooub 43190 limcresioolb 43191 lptioo2cn 43193 lptioo1cn 43194 limclner 43199 cncfiooicclem1 43441 jumpncnp 43446 dvresioo 43469 dvbdfbdioolem1 43476 itgsin0pilem1 43498 itgsinexplem1 43502 itgsubsticclem 43523 itgiccshift 43528 itgperiod 43529 itgsbtaddcnst 43530 dirkeritg 43650 dirkercncflem2 43652 dirkercncflem3 43653 dirkercncflem4 43654 dirkercncf 43655 fourierdlem28 43683 fourierdlem32 43687 fourierdlem33 43688 fourierdlem39 43694 fourierdlem56 43710 fourierdlem57 43711 fourierdlem58 43712 fourierdlem59 43713 fourierdlem62 43716 fourierdlem68 43722 fourierdlem72 43726 fourierdlem73 43727 fourierdlem74 43728 fourierdlem75 43729 fourierdlem80 43734 fourierdlem94 43748 fourierdlem103 43757 fourierdlem104 43758 fourierdlem113 43767 fouriercnp 43774 fouriersw 43779 fouriercn 43780 etransclem2 43784 etransclem23 43805 etransclem35 43817 etransclem38 43820 etransclem39 43821 etransclem44 43826 etransclem45 43827 etransclem46 43828 etransclem47 43829

W3C validator