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

Theorem topontop 16664
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 16663 . 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 1623    e. wcel 1684   U.cuni 3827   ` cfv 5255   Topctop 16631  TopOnctopon 16632
This theorem is referenced by:  toponmax  16666  topontopi  16669  topgele  16672  istps  16674  en2top  16723  pptbas  16745  toponmre  16830  cldmreon  16831  iscldtop  16832  resttopon  16892  resttopon2  16899  restlp  16913  restperf  16914  perfopn  16915  ordtopn3  16926  ordtcld1  16927  ordtcld2  16928  ordttop  16930  lmfval  16962  cnfval  16963  cnpfval  16964  tgcn  16982  tgcnp  16983  subbascn  16984  iscncl  16998  cncls2  17002  cncls  17003  cnntr  17004  cncnp  17009  cnindis  17020  lmcls  17030  iscnrm2  17066  ist0-2  17072  ist1-2  17075  ishaus2  17079  hausnei2  17081  isreg2  17105  sscmp  17132  dfcon2  17145  clscon  17156  concompcld  17160  1stccnp  17188  kgenval  17230  kgenftop  17235  1stckgenlem  17248  kgen2ss  17250  txtopon  17286  pttopon  17291  txcls  17299  ptclsg  17309  dfac14lem  17311  xkoccn  17313  txcnp  17314  ptcnplem  17315  txlm  17342  cnmpt2res  17371  cnmptkp  17374  cnmptk1  17375  cnmpt1k  17376  cnmptkk  17377  cnmptk1p  17379  cnmptk2  17380  xkoinjcn  17381  qtoptopon  17395  qtopcld  17404  qtoprest  17408  qtopcmap  17410  kqval  17417  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  kqtop  17436  pt1hmeo  17497  xpstopnlem1  17500  xkohmeo  17506  neifil  17575  trnei  17587  elflim  17666  flimss1  17668  flimopn  17670  fbflim2  17672  flimcf  17677  flimclslem  17679  flffval  17684  flfnei  17686  flftg  17691  cnpflf2  17695  isfcls2  17708  fclsopn  17709  fclsnei  17714  fclscf  17720  fclscmp  17725  fcfval  17728  fcfnei  17730  cnpfcf  17736  tgpmulg2  17777  tmdgsum  17778  tmdgsum2  17779  subgntr  17789  opnsubg  17790  clssubg  17791  clsnsg  17792  cldsubg  17793  snclseqg  17798  tgphaus  17799  divstgpopn  17802  prdstgpd  17807  tsmsgsum  17821  tsmsid  17822  tgptsmscld  17833  mopntop  17986  metdseq0  18358  cnmpt2pc  18426  ishtpy  18470  om1val  18528  pi1val  18535  csscld  18676  clsocv  18677  relcmpcmet  18742  bcth2  18752  limcres  19236  perfdvf  19253  dvaddbr  19287  dvmulbr  19288  dvcmulf  19294  dvmptres2  19311  dvmptcmul  19313  dvmptntr  19320  dvcnvlem  19323  lhop2  19362  lhop  19363  dvcnvrelem2  19365  taylthlem1  19752  iscnp4  25563  locfincf  26306  neibastop2  26310  neibastop3  26311  topjoin  26314  istopclsd  26775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fv 5263  df-topon 16639
  Copyright terms: Public domain W3C validator