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

Theorem topontop 16770
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 16769 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 446 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1642    e. wcel 1710   U.cuni 3908   ` cfv 5337   Topctop 16737  TopOnctopon 16738
This theorem is referenced by:  toponmax  16772  topontopi  16775  topgele  16778  istps  16780  en2top  16829  pptbas  16851  toponmre  16936  cldmreon  16937  iscldtop  16938  resttopon  16998  resttopon2  17005  restlp  17019  restperf  17020  perfopn  17021  ordtopn3  17032  ordtcld1  17033  ordtcld2  17034  ordttop  17036  lmfval  17068  cnfval  17069  cnpfval  17070  tgcn  17088  tgcnp  17089  subbascn  17090  iscncl  17104  cncls2  17108  cncls  17109  cnntr  17110  cncnp  17115  cnindis  17126  lmcls  17136  iscnrm2  17172  ist0-2  17178  ist1-2  17181  ishaus2  17185  hausnei2  17187  isreg2  17211  sscmp  17238  dfcon2  17251  clscon  17262  concompcld  17266  1stccnp  17294  kgenval  17336  kgenftop  17341  1stckgenlem  17354  kgen2ss  17356  txtopon  17392  pttopon  17397  txcls  17405  ptclsg  17415  dfac14lem  17417  xkoccn  17419  txcnp  17420  ptcnplem  17421  txlm  17448  cnmpt2res  17477  cnmptkp  17480  cnmptk1  17481  cnmpt1k  17482  cnmptkk  17483  cnmptk1p  17485  cnmptk2  17486  xkoinjcn  17487  qtoptopon  17501  qtopcld  17510  qtoprest  17514  qtopcmap  17516  kqval  17523  regr1lem  17536  kqreglem1  17538  kqreglem2  17539  kqnrmlem1  17540  kqnrmlem2  17541  kqtop  17542  pt1hmeo  17603  xpstopnlem1  17606  xkohmeo  17612  neifil  17677  trnei  17689  elflim  17768  flimss1  17770  flimopn  17772  fbflim2  17774  flimcf  17779  flimclslem  17781  flffval  17786  flfnei  17788  flftg  17793  cnpflf2  17797  isfcls2  17810  fclsopn  17811  fclsnei  17816  fclscf  17822  fclscmp  17827  fcfval  17830  fcfnei  17832  cnpfcf  17838  tgpmulg2  17879  tmdgsum  17880  tmdgsum2  17881  subgntr  17891  opnsubg  17892  clssubg  17893  clsnsg  17894  cldsubg  17895  snclseqg  17900  tgphaus  17901  divstgpopn  17904  prdstgpd  17909  tsmsgsum  17923  tsmsid  17924  tgptsmscld  17935  mopntop  18088  metdseq0  18461  cnmpt2pc  18530  ishtpy  18574  om1val  18632  pi1val  18639  csscld  18780  clsocv  18781  relcmpcmet  18846  bcth2  18856  limcres  19340  perfdvf  19357  dvaddbr  19391  dvmulbr  19392  dvcmulf  19398  dvmptres2  19415  dvmptcmul  19417  dvmptntr  19424  dvcnvlem  19427  lhop2  19466  lhop  19467  dvcnvrelem2  19469  taylthlem1  19856  neiptopreu  23446  iscnp4  23447  locfincf  25630  neibastop2  25634  neibastop3  25635  topjoin  25638  istopclsd  26098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-iota 5301  df-fun 5339  df-fv 5345  df-topon 16745
  Copyright terms: Public domain W3C validator