![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > topontop | Structured version Visualization version GIF version |
Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
topontop | ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | istopon 21227 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simplbi 490 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ∪ cuni 4713 ‘cfv 6190 Topctop 21208 TopOnctopon 21225 |
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 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5061 ax-nul 5068 ax-pow 5120 ax-pr 5187 ax-un 7281 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2583 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3684 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-nul 4181 df-if 4352 df-pw 4425 df-sn 4443 df-pr 4445 df-op 4449 df-uni 4714 df-br 4931 df-opab 4993 df-mpt 5010 df-id 5313 df-xp 5414 df-rel 5415 df-cnv 5416 df-co 5417 df-dm 5418 df-iota 6154 df-fun 6192 df-fv 6198 df-topon 21226 |
This theorem is referenced by: topontopi 21230 topontopon 21234 toprntopon 21240 toponmax 21241 topgele 21245 istps 21249 en2top 21300 pptbas 21323 toponmre 21408 cldmreon 21409 iscldtop 21410 neiptopreu 21448 resttopon 21476 resttopon2 21483 restlp 21498 restperf 21499 perfopn 21500 ordtopn3 21511 ordtcld1 21512 ordtcld2 21513 ordttop 21515 lmfval 21547 cnfval 21548 cnpfval 21549 tgcn 21567 tgcnp 21568 subbascn 21569 iscnp4 21578 iscncl 21584 cncls2 21588 cncls 21589 cnntr 21590 cncnp 21595 cnindis 21607 lmcls 21617 iscnrm2 21653 ist0-2 21659 ist1-2 21662 ishaus2 21666 hausnei2 21668 isreg2 21692 sscmp 21720 dfconn2 21734 clsconn 21745 conncompcld 21749 1stccnp 21777 locfincf 21846 kgenval 21850 kgenftop 21855 1stckgenlem 21868 kgen2ss 21870 txtopon 21906 pttopon 21911 txcls 21919 ptclsg 21930 dfac14lem 21932 xkoccn 21934 txcnp 21935 ptcnplem 21936 txlm 21963 cnmpt2res 21992 cnmptkp 21995 cnmptk1 21996 cnmpt1k 21997 cnmptkk 21998 cnmptk1p 22000 cnmptk2 22001 xkoinjcn 22002 qtoptopon 22019 qtopcld 22028 qtoprest 22032 qtopcmap 22034 kqval 22041 regr1lem 22054 kqreglem1 22056 kqreglem2 22057 kqnrmlem1 22058 kqnrmlem2 22059 kqtop 22060 pt1hmeo 22121 xpstopnlem1 22124 xkohmeo 22130 neifil 22195 trnei 22207 elflim 22286 flimss1 22288 flimopn 22290 fbflim2 22292 flimcf 22297 flimclslem 22299 flffval 22304 flfnei 22306 flftg 22311 cnpflf2 22315 isfcls2 22328 fclsopn 22329 fclsnei 22334 fclscf 22340 fclscmp 22345 fcfval 22348 fcfnei 22350 cnpfcf 22356 tgpmulg2 22409 tmdgsum 22410 tmdgsum2 22411 subgntr 22421 opnsubg 22422 clssubg 22423 clsnsg 22424 cldsubg 22425 snclseqg 22430 tgphaus 22431 qustgpopn 22434 prdstgpd 22439 tsmsgsum 22453 tsmsid 22454 tgptsmscld 22465 mopntop 22756 metdseq0 23168 cnmpopc 23238 ishtpy 23282 om1val 23340 pi1val 23347 csscld 23558 clsocv 23559 relcmpcmet 23627 bcth2 23639 limcres 24190 perfdvf 24207 dvaddbr 24241 dvmulbr 24242 dvcmulf 24248 dvmptres2 24265 dvmptcmul 24267 dvmptntr 24274 dvcnvlem 24279 lhop2 24318 lhop 24319 dvcnvrelem2 24321 taylthlem1 24667 neibastop2 33230 neibastop3 33231 topjoin 33234 dissneqlem 34063 istopclsd 38692 dvresntr 41633 |
Copyright terms: Public domain | W3C validator |