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

Theorem topontop 16950
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 16949 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 447 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    e. wcel 1721   U.cuni 3979   ` cfv 5417   Topctop 16917  TopOnctopon 16918
This theorem is referenced by:  toponmax  16952  topontopi  16955  topgele  16958  istps  16960  en2top  17009  pptbas  17031  toponmre  17116  cldmreon  17117  iscldtop  17118  neiptopreu  17156  resttopon  17183  resttopon2  17190  restlp  17205  restperf  17206  perfopn  17207  ordtopn3  17218  ordtcld1  17219  ordtcld2  17220  ordttop  17222  lmfval  17254  cnfval  17255  cnpfval  17256  tgcn  17274  tgcnp  17275  subbascn  17276  iscnp4  17285  iscncl  17291  cncls2  17295  cncls  17296  cnntr  17297  cncnp  17302  cnindis  17314  lmcls  17324  iscnrm2  17360  ist0-2  17366  ist1-2  17369  ishaus2  17373  hausnei2  17375  isreg2  17399  sscmp  17426  dfcon2  17439  clscon  17450  concompcld  17454  1stccnp  17482  kgenval  17524  kgenftop  17529  1stckgenlem  17542  kgen2ss  17544  txtopon  17580  pttopon  17585  txcls  17593  ptclsg  17604  dfac14lem  17606  xkoccn  17608  txcnp  17609  ptcnplem  17610  txlm  17637  cnmpt2res  17666  cnmptkp  17669  cnmptk1  17670  cnmpt1k  17671  cnmptkk  17672  cnmptk1p  17674  cnmptk2  17675  xkoinjcn  17676  qtoptopon  17693  qtopcld  17702  qtoprest  17706  qtopcmap  17708  kqval  17715  regr1lem  17728  kqreglem1  17730  kqreglem2  17731  kqnrmlem1  17732  kqnrmlem2  17733  kqtop  17734  pt1hmeo  17795  xpstopnlem1  17798  xkohmeo  17804  neifil  17869  trnei  17881  elflim  17960  flimss1  17962  flimopn  17964  fbflim2  17966  flimcf  17971  flimclslem  17973  flffval  17978  flfnei  17980  flftg  17985  cnpflf2  17989  isfcls2  18002  fclsopn  18003  fclsnei  18008  fclscf  18014  fclscmp  18019  fcfval  18022  fcfnei  18024  cnpfcf  18030  tgpmulg2  18081  tmdgsum  18082  tmdgsum2  18083  subgntr  18093  opnsubg  18094  clssubg  18095  clsnsg  18096  cldsubg  18097  snclseqg  18102  tgphaus  18103  divstgpopn  18106  prdstgpd  18111  tsmsgsum  18125  tsmsid  18126  tgptsmscld  18137  mopntop  18427  metdseq0  18841  cnmpt2pc  18910  ishtpy  18954  om1val  19012  pi1val  19019  csscld  19160  clsocv  19161  relcmpcmet  19226  bcth2  19240  limcres  19730  perfdvf  19747  dvaddbr  19781  dvmulbr  19782  dvcmulf  19788  dvmptres2  19805  dvmptcmul  19807  dvmptntr  19814  dvcnvlem  19817  lhop2  19856  lhop  19857  dvcnvrelem2  19859  taylthlem1  20246  locfincf  26280  neibastop2  26284  neibastop3  26285  topjoin  26288  istopclsd  26648
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-iota 5381  df-fun 5419  df-fv 5425  df-topon 16925
  Copyright terms: Public domain W3C validator