![]() |
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 22858 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simplbi 496 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ∪ cuni 4909 ‘cfv 6549 Topctop 22839 TopOnctopon 22856 |
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-sep 5300 ax-nul 5307 ax-pow 5365 ax-pr 5429 ax-un 7741 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 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-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4323 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5576 df-xp 5684 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-iota 6501 df-fun 6551 df-fv 6557 df-topon 22857 |
This theorem is referenced by: topontopi 22861 topontopon 22865 toprntopon 22871 toponmax 22872 topgele 22876 istps 22880 en2top 22932 pptbas 22955 toponmre 23041 cldmreon 23042 iscldtop 23043 neiptopreu 23081 resttopon 23109 resttopon2 23116 restlp 23131 restperf 23132 perfopn 23133 ordtopn3 23144 ordtcld1 23145 ordtcld2 23146 ordttop 23148 lmfval 23180 cnfval 23181 cnpfval 23182 tgcn 23200 tgcnp 23201 subbascn 23202 iscnp4 23211 iscncl 23217 cncls2 23221 cncls 23222 cnntr 23223 cncnp 23228 cnindis 23240 lmcls 23250 iscnrm2 23286 ist0-2 23292 ist1-2 23295 ishaus2 23299 hausnei2 23301 isreg2 23325 sscmp 23353 dfconn2 23367 clsconn 23378 conncompcld 23382 1stccnp 23410 locfincf 23479 kgenval 23483 kgenftop 23488 1stckgenlem 23501 kgen2ss 23503 txtopon 23539 pttopon 23544 txcls 23552 ptclsg 23563 dfac14lem 23565 xkoccn 23567 txcnp 23568 ptcnplem 23569 txlm 23596 cnmpt2res 23625 cnmptkp 23628 cnmptk1 23629 cnmpt1k 23630 cnmptkk 23631 cnmptk1p 23633 cnmptk2 23634 xkoinjcn 23635 qtoptopon 23652 qtopcld 23661 qtoprest 23665 qtopcmap 23667 kqval 23674 regr1lem 23687 kqreglem1 23689 kqreglem2 23690 kqnrmlem1 23691 kqnrmlem2 23692 kqtop 23693 pt1hmeo 23754 xpstopnlem1 23757 xkohmeo 23763 neifil 23828 trnei 23840 elflim 23919 flimss1 23921 flimopn 23923 fbflim2 23925 flimcf 23930 flimclslem 23932 flffval 23937 flfnei 23939 flftg 23944 cnpflf2 23948 isfcls2 23961 fclsopn 23962 fclsnei 23967 fclscf 23973 fclscmp 23978 fcfval 23981 fcfnei 23983 cnpfcf 23989 tgpmulg2 24042 tmdgsum 24043 tmdgsum2 24044 subgntr 24055 opnsubg 24056 clssubg 24057 clsnsg 24058 cldsubg 24059 snclseqg 24064 tgphaus 24065 qustgpopn 24068 prdstgpd 24073 tsmsgsum 24087 tsmsid 24088 tgptsmscld 24099 mopntop 24390 metdseq0 24814 cnmpopc 24893 ishtpy 24942 om1val 25001 pi1val 25008 csscld 25221 clsocv 25222 relcmpcmet 25290 bcth2 25302 limcres 25859 perfdvf 25876 dvaddbr 25912 dvmulbr 25913 dvmulbrOLD 25914 dvcmulf 25920 dvmptres2 25938 dvmptcmul 25940 dvmptntr 25947 dvcnvlem 25952 lhop2 25992 lhop 25993 dvcnvrelem2 25995 taylthlem1 26353 zartop 33608 neibastop2 35976 neibastop3 35977 topjoin 35980 dissneqlem 36950 istopclsd 42262 dvresntr 45444 |
Copyright terms: Public domain | W3C validator |