![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > retop | Structured version Visualization version GIF version |
Description: The standard topology on the reals. (Contributed by FL, 4-Jun-2007.) |
Ref | Expression |
---|---|
retop | ⊢ (topGen‘ran (,)) ∈ Top |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | retopbas 23057 | . 2 ⊢ ran (,) ∈ TopBases | |
2 | tgcl 21266 | . 2 ⊢ (ran (,) ∈ TopBases → (topGen‘ran (,)) ∈ Top) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (topGen‘ran (,)) ∈ Top |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 ran crn 5449 ‘cfv 6230 (,)cioo 12593 topGenctg 16545 Topctop 21190 TopBasesctb 21242 |
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-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 ax-cnex 10444 ax-resscn 10445 ax-pre-lttri 10462 ax-pre-lttrn 10463 |
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-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-po 5367 df-so 5368 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-ov 7024 df-oprab 7025 df-mpo 7026 df-1st 7550 df-2nd 7551 df-er 8144 df-en 8363 df-dom 8364 df-sdom 8365 df-pnf 10528 df-mnf 10529 df-xr 10530 df-ltxr 10531 df-le 10532 df-ioo 12597 df-topgen 16551 df-top 21191 df-bases 21243 |
This theorem is referenced by: retopon 23060 retps 23061 icccld 23063 icopnfcld 23064 iocmnfcld 23065 qdensere 23066 zcld 23109 iccntr 23117 icccmp 23121 reconnlem2 23123 retopconn 23125 rectbntr0 23128 cnmpopc 23220 icoopnst 23231 iocopnst 23232 cnheiborlem 23246 bndth 23250 pcoass 23316 evthicc 23748 ovolicc2 23811 subopnmbl 23893 dvlip 24278 dvlip2 24280 dvne0 24296 lhop2 24300 lhop 24301 dvcnvrelem2 24303 dvcnvre 24304 ftc1 24327 taylthlem2 24650 cxpcn3 25015 lgamgulmlem2 25294 circtopn 30723 tpr2rico 30777 rrhqima 30877 rrhre 30884 brsiga 31064 unibrsiga 31067 elmbfmvol2 31147 sxbrsigalem3 31152 dya2iocbrsiga 31155 dya2icobrsiga 31156 dya2iocucvr 31164 sxbrsigalem1 31165 orrvcval4 31344 orrvcoel 31345 orrvccel 31346 retopsconn 32111 iccllysconn 32112 rellysconn 32113 cvmliftlem8 32154 cvmliftlem10 32156 ivthALT 33299 ptrecube 34449 poimirlem29 34478 poimirlem30 34479 poimirlem31 34480 poimir 34482 broucube 34483 mblfinlem1 34486 mblfinlem2 34487 mblfinlem3 34488 mblfinlem4 34489 ismblfin 34490 cnambfre 34497 ftc1cnnc 34523 reopn 41122 ioontr 41355 iocopn 41364 icoopn 41369 limciccioolb 41470 limcicciooub 41486 lptre2pt 41489 limcresiooub 41491 limcresioolb 41492 limclner 41500 limclr 41504 icccncfext 41738 cncfiooicclem1 41744 fperdvper 41771 stoweidlem53 41907 stoweidlem57 41911 dirkercncflem2 41958 dirkercncflem3 41959 dirkercncflem4 41960 fourierdlem32 41993 fourierdlem33 41994 fourierdlem42 42003 fourierdlem48 42008 fourierdlem49 42009 fourierdlem58 42018 fourierdlem62 42022 fourierdlem73 42033 fouriersw 42085 iooborel 42203 bor1sal 42207 incsmf 42588 decsmf 42612 smfpimbor1lem2 42643 smf2id 42645 smfco 42646 |
Copyright terms: Public domain | W3C validator |