Theorem topontop 22859

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 22858	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simplbi 496	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top)

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ∪ cuni 4909  ‘cfv 6549  Topctop 22839  TopOnctopon 22856

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 2696  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741

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 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5576  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-iota 6501  df-fun 6551  df-fv 6557  df-topon 22857

This theorem is referenced by:  topontopi  22861  topontopon  22865  toprntopon  22871  toponmax  22872  topgele  22876  istps  22880  en2top  22932  pptbas  22955  toponmre  23041  cldmreon  23042  iscldtop  23043  neiptopreu  23081  resttopon  23109  resttopon2  23116  restlp  23131  restperf  23132  perfopn  23133  ordtopn3  23144  ordtcld1  23145  ordtcld2  23146  ordttop  23148  lmfval  23180  cnfval  23181  cnpfval  23182  tgcn  23200  tgcnp  23201  subbascn  23202  iscnp4  23211  iscncl  23217  cncls2  23221  cncls  23222  cnntr  23223  cncnp  23228  cnindis  23240  lmcls  23250  iscnrm2  23286  ist0-2  23292  ist1-2  23295  ishaus2  23299  hausnei2  23301  isreg2  23325  sscmp  23353  dfconn2  23367  clsconn  23378  conncompcld  23382  1stccnp  23410  locfincf  23479  kgenval  23483  kgenftop  23488  1stckgenlem  23501  kgen2ss  23503  txtopon  23539  pttopon  23544  txcls  23552  ptclsg  23563  dfac14lem  23565  xkoccn  23567  txcnp  23568  ptcnplem  23569  txlm  23596  cnmpt2res  23625  cnmptkp  23628  cnmptk1  23629  cnmpt1k  23630  cnmptkk  23631  cnmptk1p  23633  cnmptk2  23634  xkoinjcn  23635  qtoptopon  23652  qtopcld  23661  qtoprest  23665  qtopcmap  23667  kqval  23674  regr1lem  23687  kqreglem1  23689  kqreglem2  23690  kqnrmlem1  23691  kqnrmlem2  23692  kqtop  23693  pt1hmeo  23754  xpstopnlem1  23757  xkohmeo  23763  neifil  23828  trnei  23840  elflim  23919  flimss1  23921  flimopn  23923  fbflim2  23925  flimcf  23930  flimclslem  23932  flffval  23937  flfnei  23939  flftg  23944  cnpflf2  23948  isfcls2  23961  fclsopn  23962  fclsnei  23967  fclscf  23973  fclscmp  23978  fcfval  23981  fcfnei  23983  cnpfcf  23989  tgpmulg2  24042  tmdgsum  24043  tmdgsum2  24044  subgntr  24055  opnsubg  24056  clssubg  24057  clsnsg  24058  cldsubg  24059  snclseqg  24064  tgphaus  24065  qustgpopn  24068  prdstgpd  24073  tsmsgsum  24087  tsmsid  24088  tgptsmscld  24099  mopntop  24390  metdseq0  24814  cnmpopc  24893  ishtpy  24942  om1val  25001  pi1val  25008  csscld  25221  clsocv  25222  relcmpcmet  25290  bcth2  25302  limcres  25859  perfdvf  25876  dvaddbr  25912  dvmulbr  25913  dvmulbrOLD  25914  dvcmulf  25920  dvmptres2  25938  dvmptcmul  25940  dvmptntr  25947  dvcnvlem  25952  lhop2  25992  lhop  25993  dvcnvrelem2  25995  taylthlem1  26353  zartop  33608  neibastop2  35976  neibastop3  35977  topjoin  35980  dissneqlem  36950  istopclsd  42262  dvresntr  45444