Theorem topontop 22414

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∪ cuni 4908  ‘cfv 6543  Topctop 22394  TopOnctopon 22411

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-topon 22412

This theorem is referenced by:  topontopi  22416  topontopon  22420  toprntopon  22426  toponmax  22427  topgele  22431  istps  22435  en2top  22487  pptbas  22510  toponmre  22596  cldmreon  22597  iscldtop  22598  neiptopreu  22636  resttopon  22664  resttopon2  22671  restlp  22686  restperf  22687  perfopn  22688  ordtopn3  22699  ordtcld1  22700  ordtcld2  22701  ordttop  22703  lmfval  22735  cnfval  22736  cnpfval  22737  tgcn  22755  tgcnp  22756  subbascn  22757  iscnp4  22766  iscncl  22772  cncls2  22776  cncls  22777  cnntr  22778  cncnp  22783  cnindis  22795  lmcls  22805  iscnrm2  22841  ist0-2  22847  ist1-2  22850  ishaus2  22854  hausnei2  22856  isreg2  22880  sscmp  22908  dfconn2  22922  clsconn  22933  conncompcld  22937  1stccnp  22965  locfincf  23034  kgenval  23038  kgenftop  23043  1stckgenlem  23056  kgen2ss  23058  txtopon  23094  pttopon  23099  txcls  23107  ptclsg  23118  dfac14lem  23120  xkoccn  23122  txcnp  23123  ptcnplem  23124  txlm  23151  cnmpt2res  23180  cnmptkp  23183  cnmptk1  23184  cnmpt1k  23185  cnmptkk  23186  cnmptk1p  23188  cnmptk2  23189  xkoinjcn  23190  qtoptopon  23207  qtopcld  23216  qtoprest  23220  qtopcmap  23222  kqval  23229  regr1lem  23242  kqreglem1  23244  kqreglem2  23245  kqnrmlem1  23246  kqnrmlem2  23247  kqtop  23248  pt1hmeo  23309  xpstopnlem1  23312  xkohmeo  23318  neifil  23383  trnei  23395  elflim  23474  flimss1  23476  flimopn  23478  fbflim2  23480  flimcf  23485  flimclslem  23487  flffval  23492  flfnei  23494  flftg  23499  cnpflf2  23503  isfcls2  23516  fclsopn  23517  fclsnei  23522  fclscf  23528  fclscmp  23533  fcfval  23536  fcfnei  23538  cnpfcf  23544  tgpmulg2  23597  tmdgsum  23598  tmdgsum2  23599  subgntr  23610  opnsubg  23611  clssubg  23612  clsnsg  23613  cldsubg  23614  snclseqg  23619  tgphaus  23620  qustgpopn  23623  prdstgpd  23628  tsmsgsum  23642  tsmsid  23643  tgptsmscld  23654  mopntop  23945  metdseq0  24369  cnmpopc  24443  ishtpy  24487  om1val  24545  pi1val  24552  csscld  24765  clsocv  24766  relcmpcmet  24834  bcth2  24846  limcres  25402  perfdvf  25419  dvaddbr  25454  dvmulbr  25455  dvcmulf  25461  dvmptres2  25478  dvmptcmul  25480  dvmptntr  25487  dvcnvlem  25492  lhop2  25531  lhop  25532  dvcnvrelem2  25534  taylthlem1  25884  zartop  32851  gg-dvmulbr  35170  neibastop2  35241  neibastop3  35242  topjoin  35245  dissneqlem  36216  istopclsd  41428  dvresntr  44624