Theorem topontop 21523

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∪ cuni 4840  ‘cfv 6357  Topctop 21503  TopOnctopon 21520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fv 6365  df-topon 21521

This theorem is referenced by:  topontopi  21525  topontopon  21529  toprntopon  21535  toponmax  21536  topgele  21540  istps  21544  en2top  21595  pptbas  21618  toponmre  21703  cldmreon  21704  iscldtop  21705  neiptopreu  21743  resttopon  21771  resttopon2  21778  restlp  21793  restperf  21794  perfopn  21795  ordtopn3  21806  ordtcld1  21807  ordtcld2  21808  ordttop  21810  lmfval  21842  cnfval  21843  cnpfval  21844  tgcn  21862  tgcnp  21863  subbascn  21864  iscnp4  21873  iscncl  21879  cncls2  21883  cncls  21884  cnntr  21885  cncnp  21890  cnindis  21902  lmcls  21912  iscnrm2  21948  ist0-2  21954  ist1-2  21957  ishaus2  21961  hausnei2  21963  isreg2  21987  sscmp  22015  dfconn2  22029  clsconn  22040  conncompcld  22044  1stccnp  22072  locfincf  22141  kgenval  22145  kgenftop  22150  1stckgenlem  22163  kgen2ss  22165  txtopon  22201  pttopon  22206  txcls  22214  ptclsg  22225  dfac14lem  22227  xkoccn  22229  txcnp  22230  ptcnplem  22231  txlm  22258  cnmpt2res  22287  cnmptkp  22290  cnmptk1  22291  cnmpt1k  22292  cnmptkk  22293  cnmptk1p  22295  cnmptk2  22296  xkoinjcn  22297  qtoptopon  22314  qtopcld  22323  qtoprest  22327  qtopcmap  22329  kqval  22336  regr1lem  22349  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  kqtop  22355  pt1hmeo  22416  xpstopnlem1  22419  xkohmeo  22425  neifil  22490  trnei  22502  elflim  22581  flimss1  22583  flimopn  22585  fbflim2  22587  flimcf  22592  flimclslem  22594  flffval  22599  flfnei  22601  flftg  22606  cnpflf2  22610  isfcls2  22623  fclsopn  22624  fclsnei  22629  fclscf  22635  fclscmp  22640  fcfval  22643  fcfnei  22645  cnpfcf  22651  tgpmulg2  22704  tmdgsum  22705  tmdgsum2  22706  subgntr  22717  opnsubg  22718  clssubg  22719  clsnsg  22720  cldsubg  22721  snclseqg  22726  tgphaus  22727  qustgpopn  22730  prdstgpd  22735  tsmsgsum  22749  tsmsid  22750  tgptsmscld  22761  mopntop  23052  metdseq0  23464  cnmpopc  23534  ishtpy  23578  om1val  23636  pi1val  23643  csscld  23854  clsocv  23855  relcmpcmet  23923  bcth2  23935  limcres  24486  perfdvf  24503  dvaddbr  24537  dvmulbr  24538  dvcmulf  24544  dvmptres2  24561  dvmptcmul  24563  dvmptntr  24570  dvcnvlem  24575  lhop2  24614  lhop  24615  dvcnvrelem2  24617  taylthlem1  24963  neibastop2  33711  neibastop3  33712  topjoin  33715  dissneqlem  34623  istopclsd  39304  dvresntr  42209