![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iitopon | Structured version Visualization version GIF version |
Description: The unit interval is a topological space. (Contributed by Mario Carneiro, 3-Sep-2015.) |
Ref | Expression |
---|---|
iitopon | ⊢ II ∈ (TopOn‘(0[,]1)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnxmet 23074 | . . 3 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ) | |
2 | unitssre 12694 | . . . 4 ⊢ (0[,]1) ⊆ ℝ | |
3 | ax-resscn 10384 | . . . 4 ⊢ ℝ ⊆ ℂ | |
4 | 2, 3 | sstri 3863 | . . 3 ⊢ (0[,]1) ⊆ ℂ |
5 | xmetres2 22664 | . . 3 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ (0[,]1) ⊆ ℂ) → ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (∞Met‘(0[,]1))) | |
6 | 1, 4, 5 | mp2an 679 | . 2 ⊢ ((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (∞Met‘(0[,]1)) |
7 | df-ii 23178 | . . 3 ⊢ II = (MetOpen‘((abs ∘ − ) ↾ ((0[,]1) × (0[,]1)))) | |
8 | 7 | mopntopon 22742 | . 2 ⊢ (((abs ∘ − ) ↾ ((0[,]1) × (0[,]1))) ∈ (∞Met‘(0[,]1)) → II ∈ (TopOn‘(0[,]1))) |
9 | 6, 8 | ax-mp 5 | 1 ⊢ II ∈ (TopOn‘(0[,]1)) |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2048 ⊆ wss 3825 × cxp 5398 ↾ cres 5402 ∘ ccom 5404 ‘cfv 6182 (class class class)co 6970 ℂcc 10325 ℝcr 10326 0cc0 10327 1c1 10328 − cmin 10662 [,]cicc 12550 abscabs 14444 ∞Metcxmet 20222 TopOnctopon 21212 IIcii 23176 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10383 ax-resscn 10384 ax-1cn 10385 ax-icn 10386 ax-addcl 10387 ax-addrcl 10388 ax-mulcl 10389 ax-mulrcl 10390 ax-mulcom 10391 ax-addass 10392 ax-mulass 10393 ax-distr 10394 ax-i2m1 10395 ax-1ne0 10396 ax-1rid 10397 ax-rnegex 10398 ax-rrecex 10399 ax-cnre 10400 ax-pre-lttri 10401 ax-pre-lttrn 10402 ax-pre-ltadd 10403 ax-pre-mulgt0 10404 ax-pre-sup 10405 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3678 df-csb 3783 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-pss 3841 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-iun 4788 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5305 df-eprel 5310 df-po 5319 df-so 5320 df-fr 5359 df-we 5361 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-om 7391 df-1st 7494 df-2nd 7495 df-wrecs 7743 df-recs 7805 df-rdg 7843 df-er 8081 df-map 8200 df-en 8299 df-dom 8300 df-sdom 8301 df-sup 8693 df-inf 8694 df-pnf 10468 df-mnf 10469 df-xr 10470 df-ltxr 10471 df-le 10472 df-sub 10664 df-neg 10665 df-div 11091 df-nn 11432 df-2 11496 df-3 11497 df-n0 11701 df-z 11787 df-uz 12052 df-q 12156 df-rp 12198 df-xneg 12317 df-xadd 12318 df-xmul 12319 df-icc 12554 df-seq 13178 df-exp 13238 df-cj 14309 df-re 14310 df-im 14311 df-sqrt 14445 df-abs 14446 df-topgen 16563 df-psmet 20229 df-xmet 20230 df-met 20231 df-bl 20232 df-mopn 20233 df-top 21196 df-topon 21213 df-bases 21248 df-ii 23178 |
This theorem is referenced by: iitop 23181 iiuni 23182 icchmeo 23238 htpycom 23273 htpyid 23274 htpyco1 23275 htpyco2 23276 htpycc 23277 phtpycn 23280 phtpy01 23282 isphtpy2d 23284 phtpycom 23285 phtpyid 23286 phtpyco2 23287 phtpycc 23288 reparphti 23294 pcocn 23314 pcohtpylem 23316 pcoptcl 23318 pcopt 23319 pcopt2 23320 pcoass 23321 pcorevcl 23322 pcorevlem 23323 pi1xfrf 23350 pi1xfr 23352 pi1xfrcnvlem 23353 pi1xfrcnv 23354 pi1cof 23356 pi1coghm 23358 xrge0pluscn 30784 ptpconn 32025 indispconn 32026 connpconn 32027 txsconnlem 32032 txsconn 32033 cvxsconn 32035 cvmliftlem8 32084 cvmlift2lem2 32096 cvmlift2lem3 32097 cvmlift2lem6 32100 cvmlift2lem9 32103 cvmlift2lem11 32105 cvmlift2lem12 32106 cvmliftphtlem 32109 cvmlift3lem6 32116 cvmlift3lem9 32119 |
Copyright terms: Public domain | W3C validator |