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

Theorem topontop 19405
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 19404 . 2  |-  ( J  e.  (TopOn `  B
)  <->  ( J  e. 
Top  /\  B  =  U. J ) )
21simplbi 460 1  |-  ( J  e.  (TopOn `  B
)  ->  J  e.  Top )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    e. wcel 1804   U.cuni 4234   ` cfv 5578   Topctop 19372  TopOnctopon 19373
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-iota 5541  df-fun 5580  df-fv 5586  df-topon 19380
This theorem is referenced by:  toponmax  19407  topontopi  19410  topgele  19413  istps  19415  en2top  19465  pptbas  19487  toponmre  19572  cldmreon  19573  iscldtop  19574  neiptopreu  19612  resttopon  19640  resttopon2  19647  restlp  19662  restperf  19663  perfopn  19664  ordtopn3  19675  ordtcld1  19676  ordtcld2  19677  ordttop  19679  lmfval  19711  cnfval  19712  cnpfval  19713  tgcn  19731  tgcnp  19732  subbascn  19733  iscnp4  19742  iscncl  19748  cncls2  19752  cncls  19753  cnntr  19754  cncnp  19759  cnindis  19771  lmcls  19781  iscnrm2  19817  ist0-2  19823  ist1-2  19826  ishaus2  19830  hausnei2  19832  isreg2  19856  sscmp  19883  dfcon2  19898  clscon  19909  concompcld  19913  1stccnp  19941  locfincf  20010  kgenval  20014  kgenftop  20019  1stckgenlem  20032  kgen2ss  20034  txtopon  20070  pttopon  20075  txcls  20083  ptclsg  20094  dfac14lem  20096  xkoccn  20098  txcnp  20099  ptcnplem  20100  txlm  20127  cnmpt2res  20156  cnmptkp  20159  cnmptk1  20160  cnmpt1k  20161  cnmptkk  20162  cnmptk1p  20164  cnmptk2  20165  xkoinjcn  20166  qtoptopon  20183  qtopcld  20192  qtoprest  20196  qtopcmap  20198  kqval  20205  regr1lem  20218  kqreglem1  20220  kqreglem2  20221  kqnrmlem1  20222  kqnrmlem2  20223  kqtop  20224  pt1hmeo  20285  xpstopnlem1  20288  xkohmeo  20294  neifil  20359  trnei  20371  elflim  20450  flimss1  20452  flimopn  20454  fbflim2  20456  flimcf  20461  flimclslem  20463  flffval  20468  flfnei  20470  flftg  20475  cnpflf2  20479  isfcls2  20492  fclsopn  20493  fclsnei  20498  fclscf  20504  fclscmp  20509  fcfval  20512  fcfnei  20514  cnpfcf  20520  tgpmulg2  20571  tmdgsum  20572  tmdgsum2  20573  subgntr  20583  opnsubg  20584  clssubg  20585  clsnsg  20586  cldsubg  20587  snclseqg  20592  tgphaus  20593  qustgpopn  20596  prdstgpd  20601  tsmsgsum  20615  tsmsid  20616  tsmsgsumOLD  20618  tsmsidOLD  20619  tgptsmscld  20631  mopntop  20921  metdseq0  21336  cnmpt2pc  21406  ishtpy  21450  om1val  21508  pi1val  21515  csscld  21667  clsocv  21668  relcmpcmet  21733  bcth2  21747  limcres  22268  perfdvf  22285  dvaddbr  22319  dvmulbr  22320  dvcmulf  22326  dvmptres2  22343  dvmptcmul  22345  dvmptntr  22352  dvcnvlem  22355  lhop2  22394  lhop  22395  dvcnvrelem2  22397  taylthlem1  22746  neibastop2  30155  neibastop3  30156  topjoin  30159  istopclsd  30608  dvresntr  31667
  Copyright terms: Public domain W3C validator