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

Theorem topontop 19865
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 19864 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 461 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    e. wcel 1867   U.cuni 4213   ` cfv 5592   Topctop 19841  TopOnctopon 19842
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-iota 5556  df-fun 5594  df-fv 5600  df-topon 19847
This theorem is referenced by:  toponmax  19867  topontopi  19870  topgele  19873  istps  19875  en2top  19925  pptbas  19947  toponmre  20033  cldmreon  20034  iscldtop  20035  neiptopreu  20073  resttopon  20101  resttopon2  20108  restlp  20123  restperf  20124  perfopn  20125  ordtopn3  20136  ordtcld1  20137  ordtcld2  20138  ordttop  20140  lmfval  20172  cnfval  20173  cnpfval  20174  tgcn  20192  tgcnp  20193  subbascn  20194  iscnp4  20203  iscncl  20209  cncls2  20213  cncls  20214  cnntr  20215  cncnp  20220  cnindis  20232  lmcls  20242  iscnrm2  20278  ist0-2  20284  ist1-2  20287  ishaus2  20291  hausnei2  20293  isreg2  20317  sscmp  20344  dfcon2  20358  clscon  20369  concompcld  20373  1stccnp  20401  locfincf  20470  kgenval  20474  kgenftop  20479  1stckgenlem  20492  kgen2ss  20494  txtopon  20530  pttopon  20535  txcls  20543  ptclsg  20554  dfac14lem  20556  xkoccn  20558  txcnp  20559  ptcnplem  20560  txlm  20587  cnmpt2res  20616  cnmptkp  20619  cnmptk1  20620  cnmpt1k  20621  cnmptkk  20622  cnmptk1p  20624  cnmptk2  20625  xkoinjcn  20626  qtoptopon  20643  qtopcld  20652  qtoprest  20656  qtopcmap  20658  kqval  20665  regr1lem  20678  kqreglem1  20680  kqreglem2  20681  kqnrmlem1  20682  kqnrmlem2  20683  kqtop  20684  pt1hmeo  20745  xpstopnlem1  20748  xkohmeo  20754  neifil  20819  trnei  20831  elflim  20910  flimss1  20912  flimopn  20914  fbflim2  20916  flimcf  20921  flimclslem  20923  flffval  20928  flfnei  20930  flftg  20935  cnpflf2  20939  isfcls2  20952  fclsopn  20953  fclsnei  20958  fclscf  20964  fclscmp  20969  fcfval  20972  fcfnei  20974  cnpfcf  20980  tgpmulg2  21033  tmdgsum  21034  tmdgsum2  21035  subgntr  21045  opnsubg  21046  clssubg  21047  clsnsg  21048  cldsubg  21049  snclseqg  21054  tgphaus  21055  qustgpopn  21058  prdstgpd  21063  tsmsgsum  21077  tsmsid  21078  tgptsmscld  21089  mopntop  21379  metdseq0  21775  cnmpt2pc  21845  ishtpy  21889  om1val  21947  pi1val  21954  csscld  22106  clsocv  22107  relcmpcmet  22172  bcth2  22184  limcres  22715  perfdvf  22732  dvaddbr  22766  dvmulbr  22767  dvcmulf  22773  dvmptres2  22790  dvmptcmul  22792  dvmptntr  22799  dvcnvlem  22802  lhop2  22841  lhop  22842  dvcnvrelem2  22844  taylthlem1  23190  neibastop2  30799  neibastop3  30800  topjoin  30803  dissneqlem  31473  istopclsd  35251  dvresntr  37364
  Copyright terms: Public domain W3C validator