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

Theorem topontop 19941
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 19940 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 462 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1444    e. wcel 1887   U.cuni 4198   ` cfv 5582   Topctop 19917  TopOnctopon 19918
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-iota 5546  df-fun 5584  df-fv 5590  df-topon 19923
This theorem is referenced by:  toponmax  19943  topontopi  19946  topgele  19949  istps  19951  en2top  20001  pptbas  20023  toponmre  20109  cldmreon  20110  iscldtop  20111  neiptopreu  20149  resttopon  20177  resttopon2  20184  restlp  20199  restperf  20200  perfopn  20201  ordtopn3  20212  ordtcld1  20213  ordtcld2  20214  ordttop  20216  lmfval  20248  cnfval  20249  cnpfval  20250  tgcn  20268  tgcnp  20269  subbascn  20270  iscnp4  20279  iscncl  20285  cncls2  20289  cncls  20290  cnntr  20291  cncnp  20296  cnindis  20308  lmcls  20318  iscnrm2  20354  ist0-2  20360  ist1-2  20363  ishaus2  20367  hausnei2  20369  isreg2  20393  sscmp  20420  dfcon2  20434  clscon  20445  concompcld  20449  1stccnp  20477  locfincf  20546  kgenval  20550  kgenftop  20555  1stckgenlem  20568  kgen2ss  20570  txtopon  20606  pttopon  20611  txcls  20619  ptclsg  20630  dfac14lem  20632  xkoccn  20634  txcnp  20635  ptcnplem  20636  txlm  20663  cnmpt2res  20692  cnmptkp  20695  cnmptk1  20696  cnmpt1k  20697  cnmptkk  20698  cnmptk1p  20700  cnmptk2  20701  xkoinjcn  20702  qtoptopon  20719  qtopcld  20728  qtoprest  20732  qtopcmap  20734  kqval  20741  regr1lem  20754  kqreglem1  20756  kqreglem2  20757  kqnrmlem1  20758  kqnrmlem2  20759  kqtop  20760  pt1hmeo  20821  xpstopnlem1  20824  xkohmeo  20830  neifil  20895  trnei  20907  elflim  20986  flimss1  20988  flimopn  20990  fbflim2  20992  flimcf  20997  flimclslem  20999  flffval  21004  flfnei  21006  flftg  21011  cnpflf2  21015  isfcls2  21028  fclsopn  21029  fclsnei  21034  fclscf  21040  fclscmp  21045  fcfval  21048  fcfnei  21050  cnpfcf  21056  tgpmulg2  21109  tmdgsum  21110  tmdgsum2  21111  subgntr  21121  opnsubg  21122  clssubg  21123  clsnsg  21124  cldsubg  21125  snclseqg  21130  tgphaus  21131  qustgpopn  21134  prdstgpd  21139  tsmsgsum  21153  tsmsid  21154  tgptsmscld  21165  mopntop  21455  metdseq0  21871  metdseq0OLD  21886  cnmpt2pc  21956  ishtpy  22003  om1val  22061  pi1val  22068  csscld  22220  clsocv  22221  relcmpcmet  22286  bcth2  22298  limcres  22841  perfdvf  22858  dvaddbr  22892  dvmulbr  22893  dvcmulf  22899  dvmptres2  22916  dvmptcmul  22918  dvmptntr  22925  dvcnvlem  22928  lhop2  22967  lhop  22968  dvcnvrelem2  22970  taylthlem1  23328  neibastop2  31017  neibastop3  31018  topjoin  31021  dissneqlem  31742  istopclsd  35542  dvresntr  37788
  Copyright terms: Public domain W3C validator