MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  topontop Structured version   Unicode version

Theorem topontop 19194
Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
topontop  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )

Proof of Theorem topontop
StepHypRef Expression
1 istopon 19193 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 460 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379    e. wcel 1767   U.cuni 4245   ` cfv 5586   Topctop 19161  TopOnctopon 19162
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-mpt 4507  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-iota 5549  df-fun 5588  df-fv 5594  df-topon 19169
This theorem is referenced by:  toponmax  19196  topontopi  19199  topgele  19202  istps  19204  en2top  19253  pptbas  19275  toponmre  19360  cldmreon  19361  iscldtop  19362  neiptopreu  19400  resttopon  19428  resttopon2  19435  restlp  19450  restperf  19451  perfopn  19452  ordtopn3  19463  ordtcld1  19464  ordtcld2  19465  ordttop  19467  lmfval  19499  cnfval  19500  cnpfval  19501  tgcn  19519  tgcnp  19520  subbascn  19521  iscnp4  19530  iscncl  19536  cncls2  19540  cncls  19541  cnntr  19542  cncnp  19547  cnindis  19559  lmcls  19569  iscnrm2  19605  ist0-2  19611  ist1-2  19614  ishaus2  19618  hausnei2  19620  isreg2  19644  sscmp  19671  dfcon2  19686  clscon  19697  concompcld  19701  1stccnp  19729  kgenval  19771  kgenftop  19776  1stckgenlem  19789  kgen2ss  19791  txtopon  19827  pttopon  19832  txcls  19840  ptclsg  19851  dfac14lem  19853  xkoccn  19855  txcnp  19856  ptcnplem  19857  txlm  19884  cnmpt2res  19913  cnmptkp  19916  cnmptk1  19917  cnmpt1k  19918  cnmptkk  19919  cnmptk1p  19921  cnmptk2  19922  xkoinjcn  19923  qtoptopon  19940  qtopcld  19949  qtoprest  19953  qtopcmap  19955  kqval  19962  regr1lem  19975  kqreglem1  19977  kqreglem2  19978  kqnrmlem1  19979  kqnrmlem2  19980  kqtop  19981  pt1hmeo  20042  xpstopnlem1  20045  xkohmeo  20051  neifil  20116  trnei  20128  elflim  20207  flimss1  20209  flimopn  20211  fbflim2  20213  flimcf  20218  flimclslem  20220  flffval  20225  flfnei  20227  flftg  20232  cnpflf2  20236  isfcls2  20249  fclsopn  20250  fclsnei  20255  fclscf  20261  fclscmp  20266  fcfval  20269  fcfnei  20271  cnpfcf  20277  tgpmulg2  20328  tmdgsum  20329  tmdgsum2  20330  subgntr  20340  opnsubg  20341  clssubg  20342  clsnsg  20343  cldsubg  20344  snclseqg  20349  tgphaus  20350  divstgpopn  20353  prdstgpd  20358  tsmsgsum  20372  tsmsid  20373  tsmsgsumOLD  20375  tsmsidOLD  20376  tgptsmscld  20388  mopntop  20678  metdseq0  21093  cnmpt2pc  21163  ishtpy  21207  om1val  21265  pi1val  21272  csscld  21424  clsocv  21425  relcmpcmet  21490  bcth2  21504  limcres  22025  perfdvf  22042  dvaddbr  22076  dvmulbr  22077  dvcmulf  22083  dvmptres2  22100  dvmptcmul  22102  dvmptntr  22109  dvcnvlem  22112  lhop2  22151  lhop  22152  dvcnvrelem2  22154  taylthlem1  22502  locfincf  29778  neibastop2  29782  neibastop3  29783  topjoin  29786  istopclsd  30236  dvresntr  31246
  Copyright terms: Public domain W3C validator