Theorem topontop 21228

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  ∪ cuni 4713  ‘cfv 6190  Topctop 21208  TopOnctopon 21225

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pow 5120  ax-pr 5187  ax-un 7281

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-pw 4425  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-mpt 5010  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-iota 6154  df-fun 6192  df-fv 6198  df-topon 21226

This theorem is referenced by:  topontopi  21230  topontopon  21234  toprntopon  21240  toponmax  21241  topgele  21245  istps  21249  en2top  21300  pptbas  21323  toponmre  21408  cldmreon  21409  iscldtop  21410  neiptopreu  21448  resttopon  21476  resttopon2  21483  restlp  21498  restperf  21499  perfopn  21500  ordtopn3  21511  ordtcld1  21512  ordtcld2  21513  ordttop  21515  lmfval  21547  cnfval  21548  cnpfval  21549  tgcn  21567  tgcnp  21568  subbascn  21569  iscnp4  21578  iscncl  21584  cncls2  21588  cncls  21589  cnntr  21590  cncnp  21595  cnindis  21607  lmcls  21617  iscnrm2  21653  ist0-2  21659  ist1-2  21662  ishaus2  21666  hausnei2  21668  isreg2  21692  sscmp  21720  dfconn2  21734  clsconn  21745  conncompcld  21749  1stccnp  21777  locfincf  21846  kgenval  21850  kgenftop  21855  1stckgenlem  21868  kgen2ss  21870  txtopon  21906  pttopon  21911  txcls  21919  ptclsg  21930  dfac14lem  21932  xkoccn  21934  txcnp  21935  ptcnplem  21936  txlm  21963  cnmpt2res  21992  cnmptkp  21995  cnmptk1  21996  cnmpt1k  21997  cnmptkk  21998  cnmptk1p  22000  cnmptk2  22001  xkoinjcn  22002  qtoptopon  22019  qtopcld  22028  qtoprest  22032  qtopcmap  22034  kqval  22041  regr1lem  22054  kqreglem1  22056  kqreglem2  22057  kqnrmlem1  22058  kqnrmlem2  22059  kqtop  22060  pt1hmeo  22121  xpstopnlem1  22124  xkohmeo  22130  neifil  22195  trnei  22207  elflim  22286  flimss1  22288  flimopn  22290  fbflim2  22292  flimcf  22297  flimclslem  22299  flffval  22304  flfnei  22306  flftg  22311  cnpflf2  22315  isfcls2  22328  fclsopn  22329  fclsnei  22334  fclscf  22340  fclscmp  22345  fcfval  22348  fcfnei  22350  cnpfcf  22356  tgpmulg2  22409  tmdgsum  22410  tmdgsum2  22411  subgntr  22421  opnsubg  22422  clssubg  22423  clsnsg  22424  cldsubg  22425  snclseqg  22430  tgphaus  22431  qustgpopn  22434  prdstgpd  22439  tsmsgsum  22453  tsmsid  22454  tgptsmscld  22465  mopntop  22756  metdseq0  23168  cnmpopc  23238  ishtpy  23282  om1val  23340  pi1val  23347  csscld  23558  clsocv  23559  relcmpcmet  23627  bcth2  23639  limcres  24190  perfdvf  24207  dvaddbr  24241  dvmulbr  24242  dvcmulf  24248  dvmptres2  24265  dvmptcmul  24267  dvmptntr  24274  dvcnvlem  24279  lhop2  24318  lhop  24319  dvcnvrelem2  24321  taylthlem1  24667  neibastop2  33230  neibastop3  33231  topjoin  33234  dissneqlem  34063  istopclsd  38692  dvresntr  41633