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

Theorem topontop 21522
Description: A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.)
Assertion
Ref Expression
topontop (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Proof of Theorem topontop
StepHypRef Expression
1 istopon 21521 . 2 (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = 𝐽))
21simplbi 501 1 (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112   cuni 4803  cfv 6328  Topctop 21502  TopOnctopon 21519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fv 6336  df-topon 21520
This theorem is referenced by:  topontopi  21524  topontopon  21528  toprntopon  21534  toponmax  21535  topgele  21539  istps  21543  en2top  21594  pptbas  21617  toponmre  21702  cldmreon  21703  iscldtop  21704  neiptopreu  21742  resttopon  21770  resttopon2  21777  restlp  21792  restperf  21793  perfopn  21794  ordtopn3  21805  ordtcld1  21806  ordtcld2  21807  ordttop  21809  lmfval  21841  cnfval  21842  cnpfval  21843  tgcn  21861  tgcnp  21862  subbascn  21863  iscnp4  21872  iscncl  21878  cncls2  21882  cncls  21883  cnntr  21884  cncnp  21889  cnindis  21901  lmcls  21911  iscnrm2  21947  ist0-2  21953  ist1-2  21956  ishaus2  21960  hausnei2  21962  isreg2  21986  sscmp  22014  dfconn2  22028  clsconn  22039  conncompcld  22043  1stccnp  22071  locfincf  22140  kgenval  22144  kgenftop  22149  1stckgenlem  22162  kgen2ss  22164  txtopon  22200  pttopon  22205  txcls  22213  ptclsg  22224  dfac14lem  22226  xkoccn  22228  txcnp  22229  ptcnplem  22230  txlm  22257  cnmpt2res  22286  cnmptkp  22289  cnmptk1  22290  cnmpt1k  22291  cnmptkk  22292  cnmptk1p  22294  cnmptk2  22295  xkoinjcn  22296  qtoptopon  22313  qtopcld  22322  qtoprest  22326  qtopcmap  22328  kqval  22335  regr1lem  22348  kqreglem1  22350  kqreglem2  22351  kqnrmlem1  22352  kqnrmlem2  22353  kqtop  22354  pt1hmeo  22415  xpstopnlem1  22418  xkohmeo  22424  neifil  22489  trnei  22501  elflim  22580  flimss1  22582  flimopn  22584  fbflim2  22586  flimcf  22591  flimclslem  22593  flffval  22598  flfnei  22600  flftg  22605  cnpflf2  22609  isfcls2  22622  fclsopn  22623  fclsnei  22628  fclscf  22634  fclscmp  22639  fcfval  22642  fcfnei  22644  cnpfcf  22650  tgpmulg2  22703  tmdgsum  22704  tmdgsum2  22705  subgntr  22716  opnsubg  22717  clssubg  22718  clsnsg  22719  cldsubg  22720  snclseqg  22725  tgphaus  22726  qustgpopn  22729  prdstgpd  22734  tsmsgsum  22748  tsmsid  22749  tgptsmscld  22760  mopntop  23051  metdseq0  23463  cnmpopc  23537  ishtpy  23581  om1val  23639  pi1val  23646  csscld  23857  clsocv  23858  relcmpcmet  23926  bcth2  23938  limcres  24493  perfdvf  24510  dvaddbr  24545  dvmulbr  24546  dvcmulf  24552  dvmptres2  24569  dvmptcmul  24571  dvmptntr  24578  dvcnvlem  24583  lhop2  24622  lhop  24623  dvcnvrelem2  24625  taylthlem1  24972  zartop  31233  neibastop2  33823  neibastop3  33824  topjoin  33827  dissneqlem  34758  istopclsd  39638  dvresntr  42557
  Copyright terms: Public domain W3C validator