![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > uniretop | Structured version Visualization version GIF version |
Description: The underlying set of the standard topology on the reals is the reals. (Contributed by FL, 4-Jun-2007.) |
Ref | Expression |
---|---|
uniretop | ⊢ ℝ = ∪ (topGen‘ran (,)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | unirnioo 12687 | . 2 ⊢ ℝ = ∪ ran (,) | |
2 | retopbas 23052 | . . 3 ⊢ ran (,) ∈ TopBases | |
3 | unitg 21259 | . . 3 ⊢ (ran (,) ∈ TopBases → ∪ (topGen‘ran (,)) = ∪ ran (,)) | |
4 | 2, 3 | ax-mp 5 | . 2 ⊢ ∪ (topGen‘ran (,)) = ∪ ran (,) |
5 | 1, 4 | eqtr4i 2821 | 1 ⊢ ℝ = ∪ (topGen‘ran (,)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2080 ∪ cuni 4747 ran crn 5447 ‘cfv 6228 ℝcr 10385 (,)cioo 12588 topGenctg 16540 TopBasesctb 21237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-pre-lttri 10460 ax-pre-lttrn 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 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-id 5351 df-po 5365 df-so 5366 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-ov 7022 df-oprab 7023 df-mpo 7024 df-1st 7548 df-2nd 7549 df-er 8142 df-en 8361 df-dom 8362 df-sdom 8363 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-ioo 12592 df-topgen 16546 df-bases 21238 |
This theorem is referenced by: retopon 23055 retps 23056 icccld 23058 icopnfcld 23059 iocmnfcld 23060 qdensere 23061 zcld 23104 iccntr 23112 icccmp 23116 retopconn 23120 opnreen 23122 rectbntr0 23123 cnmpopc 23215 evth 23246 evth2 23247 evthicc 23743 ovolicc2 23806 opnmbllem 23885 lhop 24296 dvcnvrelem2 24298 dvcnvre 24299 ftc1 24322 taylthlem2 24645 ipasslem8 28297 circtopn 30710 tpr2rico 30764 rrhf 30848 rrhqima 30864 rrhre 30871 brsigarn 31052 unibrsiga 31054 sxbrsigalem3 31139 dya2iocucvr 31151 sxbrsigalem1 31152 orrvcval4 31331 orrvcoel 31332 orrvccel 31333 retopsconn 32098 cvmliftlem10 32143 ivthALT 33286 ptrecube 34436 poimirlem29 34465 poimirlem30 34466 poimirlem31 34467 opnmbllem0 34472 mblfinlem1 34473 mblfinlem2 34474 mblfinlem3 34475 mblfinlem4 34476 ismblfin 34477 ftc1cnnc 34510 refsum2cnlem1 40846 sncldre 40856 reopn 41109 ioontr 41342 limciccioolb 41457 limcicciooub 41473 lptre2pt 41476 limclner 41487 limclr 41491 cncfiooicclem1 41731 fperdvper 41758 itgsubsticclem 41815 stoweidlem62 41903 dirkercncflem2 41945 dirkercncflem3 41946 dirkercncflem4 41947 fourierdlem42 41990 fourierdlem58 42005 fourierdlem73 42020 fouriercnp 42067 fouriercn 42073 cnfsmf 42573 incsmf 42575 decsmf 42599 smfpimbor1lem2 42630 |
Copyright terms: Public domain | W3C validator |