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 24749

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 2725	. 2 ⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) = ((abs ∘ − ) ↾ (ℝ × ℝ))
2		cnxmet 24719	. . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
3		ax-resscn 11195	. . 3 ⊢ ℝ ⊆ ℂ
4		tgioo2.1	. . . . 5 ⊢ 𝐽 = (TopOpen‘ℂ_fld)
5	4	cnfldtopn 24728	. . . 4 ⊢ 𝐽 = (MetOpen‘(abs ∘ − ))
6		eqid 2725	. . . 4 ⊢ (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
7	1, 5, 6	metrest 24463	. . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ ℝ ⊆ ℂ) → (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ))))
8	2, 3, 7	mp2an 690	. 2 ⊢ (𝐽 ↾_t ℝ) = (MetOpen‘((abs ∘ − ) ↾ (ℝ × ℝ)))
9	1, 8	tgioo 24742	1 ⊢ (topGen‘ran (,)) = (𝐽 ↾_t ℝ)

Colors of variables: wff setvar class

Syntax hints: = wceq 1533 ∈ wcel 2098 ⊆ wss 3945 × cxp 5675 ran crn 5678 ↾ cres 5679 ∘ ccom 5681 ‘cfv 6547 (class class class)co 7417 ℂcc 11136 ℝcr 11137 − cmin 11474 (,)cioo 13356 abscabs 15213 ↾_t crest 17401 TopOpenctopn 17402 topGenctg 17418 ∞Metcxmet 21268 MetOpencmopn 21273 ℂ_fldccnfld 21283

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 ax-cnex 11194 ax-resscn 11195 ax-1cn 11196 ax-icn 11197 ax-addcl 11198 ax-addrcl 11199 ax-mulcl 11200 ax-mulrcl 11201 ax-mulcom 11202 ax-addass 11203 ax-mulass 11204 ax-distr 11205 ax-i2m1 11206 ax-1ne0 11207 ax-1rid 11208 ax-rnegex 11209 ax-rrecex 11210 ax-cnre 11211 ax-pre-lttri 11212 ax-pre-lttrn 11213 ax-pre-ltadd 11214 ax-pre-mulgt0 11215 ax-pre-sup 11216

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-pss 3965 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-tp 4634 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6305 df-ord 6372 df-on 6373 df-lim 6374 df-suc 6375 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-riota 7373 df-ov 7420 df-oprab 7421 df-mpo 7422 df-om 7870 df-1st 7992 df-2nd 7993 df-frecs 8285 df-wrecs 8316 df-recs 8390 df-rdg 8429 df-1o 8485 df-er 8723 df-map 8845 df-en 8963 df-dom 8964 df-sdom 8965 df-fin 8966 df-sup 9465 df-inf 9466 df-pnf 11280 df-mnf 11281 df-xr 11282 df-ltxr 11283 df-le 11284 df-sub 11476 df-neg 11477 df-div 11902 df-nn 12243 df-2 12305 df-3 12306 df-4 12307 df-5 12308 df-6 12309 df-7 12310 df-8 12311 df-9 12312 df-n0 12503 df-z 12589 df-dec 12708 df-uz 12853 df-q 12963 df-rp 13007 df-xneg 13124 df-xadd 13125 df-xmul 13126 df-ioo 13360 df-fz 13517 df-seq 13999 df-exp 14059 df-cj 15078 df-re 15079 df-im 15080 df-sqrt 15214 df-abs 15215 df-struct 17115 df-slot 17150 df-ndx 17162 df-base 17180 df-plusg 17245 df-mulr 17246 df-starv 17247 df-tset 17251 df-ple 17252 df-ds 17254 df-unif 17255 df-rest 17403 df-topn 17404 df-topgen 17424 df-psmet 21275 df-xmet 21276 df-met 21277 df-bl 21278 df-mopn 21279 df-cnfld 21284 df-top 22826 df-topon 22843 df-bases 22879

This theorem is referenced by: rerest 24750 tgioo3 24751 zcld2 24761 metdcn 24786 ngnmcncn 24791 metdscn2 24803 abscncfALT 24875 cnrehmeo 24908 cnrehmeoOLD 24909 rellycmp 24913 evth 24915 evth2 24916 lebnumlem2 24918 resscdrg 25316 retopn 25337 cncombf 25617 cnmbf 25618 dvmptresicc 25875 dvcjbr 25911 rolle 25952 cmvth 25953 cmvthOLD 25954 mvth 25955 dvlip 25956 dvlipcn 25957 dvlip2 25958 c1liplem1 25959 dvgt0lem1 25965 dvle 25970 dvivthlem1 25971 dvne0 25974 lhop1lem 25976 lhop2 25978 lhop 25979 dvcnvrelem1 25980 dvcnvrelem2 25981 dvcnvre 25982 dvcvx 25983 dvfsumle 25984 dvfsumleOLD 25985 dvfsumabs 25987 dvfsumlem2 25991 dvfsumlem2OLD 25992 ftc1 26007 ftc1cn 26008 ftc2 26009 ftc2ditglem 26010 itgparts 26012 itgsubstlem 26013 itgpowd 26015 taylthlem2 26339 taylthlem2OLD 26340 efcvx 26416 pige3ALT 26484 dvloglem 26612 logdmopn 26613 advlog 26618 advlogexp 26619 logccv 26627 loglesqrt 26723 lgamgulmlem2 26992 ftalem3 27037 log2sumbnd 27507 nmcnc 30562 ipasslem7 30702 rmulccn 33599 raddcn 33600 ftc2re 34300 knoppcnlem10 36047 knoppcnlem11 36048 broucube 37197 ftc1cnnc 37235 ftc2nc 37245 dvasin 37247 dvacos 37248 dvreasin 37249 dvreacos 37250 areacirclem1 37251 areacirc 37256 dvrelog2 41604 dvrelog3 41605 aks4d1p1p6 41613 lhe4.4ex1a 43831 refsumcn 44457 xrtgcntopre 44924 tgioo4 45021 climreeq 45064 limcresiooub 45093 limcresioolb 45094 lptioo2cn 45096 lptioo1cn 45097 limclner 45102 cncfiooicclem1 45344 jumpncnp 45349 dvresioo 45372 dvbdfbdioolem1 45379 itgsin0pilem1 45401 itgsinexplem1 45405 itgsubsticclem 45426 itgiccshift 45431 itgperiod 45432 itgsbtaddcnst 45433 dirkeritg 45553 dirkercncflem2 45555 dirkercncflem3 45556 dirkercncflem4 45557 dirkercncf 45558 fourierdlem28 45586 fourierdlem32 45590 fourierdlem33 45591 fourierdlem39 45597 fourierdlem56 45613 fourierdlem57 45614 fourierdlem58 45615 fourierdlem59 45616 fourierdlem62 45619 fourierdlem68 45625 fourierdlem72 45629 fourierdlem73 45630 fourierdlem74 45631 fourierdlem75 45632 fourierdlem80 45637 fourierdlem94 45651 fourierdlem103 45660 fourierdlem104 45661 fourierdlem113 45670 fouriercnp 45677 fouriersw 45682 fouriercn 45683 etransclem2 45687 etransclem23 45708 etransclem35 45720 etransclem38 45723 etransclem39 45724 etransclem44 45729 etransclem45 45730 etransclem46 45731 etransclem47 45732

W3C validator