Theorem topontop 22835

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

Step	Hyp	Ref	Expression
1		istopon 22834	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simplbi 496	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ∪ cuni 4912  ‘cfv 6553  Topctop 22815  TopOnctopon 22832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7746

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-mpt 5236  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-iota 6505  df-fun 6555  df-fv 6561  df-topon 22833

This theorem is referenced by:  topontopi  22837  topontopon  22841  toprntopon  22847  toponmax  22848  topgele  22852  istps  22856  en2top  22908  pptbas  22931  toponmre  23017  cldmreon  23018  iscldtop  23019  neiptopreu  23057  resttopon  23085  resttopon2  23092  restlp  23107  restperf  23108  perfopn  23109  ordtopn3  23120  ordtcld1  23121  ordtcld2  23122  ordttop  23124  lmfval  23156  cnfval  23157  cnpfval  23158  tgcn  23176  tgcnp  23177  subbascn  23178  iscnp4  23187  iscncl  23193  cncls2  23197  cncls  23198  cnntr  23199  cncnp  23204  cnindis  23216  lmcls  23226  iscnrm2  23262  ist0-2  23268  ist1-2  23271  ishaus2  23275  hausnei2  23277  isreg2  23301  sscmp  23329  dfconn2  23343  clsconn  23354  conncompcld  23358  1stccnp  23386  locfincf  23455  kgenval  23459  kgenftop  23464  1stckgenlem  23477  kgen2ss  23479  txtopon  23515  pttopon  23520  txcls  23528  ptclsg  23539  dfac14lem  23541  xkoccn  23543  txcnp  23544  ptcnplem  23545  txlm  23572  cnmpt2res  23601  cnmptkp  23604  cnmptk1  23605  cnmpt1k  23606  cnmptkk  23607  cnmptk1p  23609  cnmptk2  23610  xkoinjcn  23611  qtoptopon  23628  qtopcld  23637  qtoprest  23641  qtopcmap  23643  kqval  23650  regr1lem  23663  kqreglem1  23665  kqreglem2  23666  kqnrmlem1  23667  kqnrmlem2  23668  kqtop  23669  pt1hmeo  23730  xpstopnlem1  23733  xkohmeo  23739  neifil  23804  trnei  23816  elflim  23895  flimss1  23897  flimopn  23899  fbflim2  23901  flimcf  23906  flimclslem  23908  flffval  23913  flfnei  23915  flftg  23920  cnpflf2  23924  isfcls2  23937  fclsopn  23938  fclsnei  23943  fclscf  23949  fclscmp  23954  fcfval  23957  fcfnei  23959  cnpfcf  23965  tgpmulg2  24018  tmdgsum  24019  tmdgsum2  24020  subgntr  24031  opnsubg  24032  clssubg  24033  clsnsg  24034  cldsubg  24035  snclseqg  24040  tgphaus  24041  qustgpopn  24044  prdstgpd  24049  tsmsgsum  24063  tsmsid  24064  tgptsmscld  24075  mopntop  24366  metdseq0  24790  cnmpopc  24869  ishtpy  24918  om1val  24977  pi1val  24984  csscld  25197  clsocv  25198  relcmpcmet  25266  bcth2  25278  limcres  25835  perfdvf  25852  dvaddbr  25888  dvmulbr  25889  dvmulbrOLD  25890  dvcmulf  25896  dvmptres2  25914  dvmptcmul  25916  dvmptntr  25923  dvcnvlem  25928  lhop2  25968  lhop  25969  dvcnvrelem2  25971  taylthlem1  26328  zartop  33510  neibastop2  35878  neibastop3  35879  topjoin  35882  dissneqlem  36852  istopclsd  42151  dvresntr  45335