Theorem topontop 22941

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2107  ∪ cuni 4913  ‘cfv 6566  Topctop 22921  TopOnctopon 22938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5303  ax-nul 5313  ax-pow 5372  ax-pr 5439  ax-un 7758

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-rab 3435  df-v 3481  df-dif 3967  df-un 3969  df-in 3971  df-ss 3981  df-nul 4341  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4914  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5584  df-xp 5696  df-rel 5697  df-cnv 5698  df-co 5699  df-dm 5700  df-iota 6519  df-fun 6568  df-fv 6574  df-topon 22939

This theorem is referenced by:  topontopi  22943  topontopon  22947  toprntopon  22953  toponmax  22954  topgele  22958  istps  22962  en2top  23014  pptbas  23037  toponmre  23123  cldmreon  23124  iscldtop  23125  neiptopreu  23163  resttopon  23191  resttopon2  23198  restlp  23213  restperf  23214  perfopn  23215  ordtopn3  23226  ordtcld1  23227  ordtcld2  23228  ordttop  23230  lmfval  23262  cnfval  23263  cnpfval  23264  tgcn  23282  tgcnp  23283  subbascn  23284  iscnp4  23293  iscncl  23299  cncls2  23303  cncls  23304  cnntr  23305  cncnp  23310  cnindis  23322  lmcls  23332  iscnrm2  23368  ist0-2  23374  ist1-2  23377  ishaus2  23381  hausnei2  23383  isreg2  23407  sscmp  23435  dfconn2  23449  clsconn  23460  conncompcld  23464  1stccnp  23492  locfincf  23561  kgenval  23565  kgenftop  23570  1stckgenlem  23583  kgen2ss  23585  txtopon  23621  pttopon  23626  txcls  23634  ptclsg  23645  dfac14lem  23647  xkoccn  23649  txcnp  23650  ptcnplem  23651  txlm  23678  cnmpt2res  23707  cnmptkp  23710  cnmptk1  23711  cnmpt1k  23712  cnmptkk  23713  cnmptk1p  23715  cnmptk2  23716  xkoinjcn  23717  qtoptopon  23734  qtopcld  23743  qtoprest  23747  qtopcmap  23749  kqval  23756  regr1lem  23769  kqreglem1  23771  kqreglem2  23772  kqnrmlem1  23773  kqnrmlem2  23774  kqtop  23775  pt1hmeo  23836  xpstopnlem1  23839  xkohmeo  23845  neifil  23910  trnei  23922  elflim  24001  flimss1  24003  flimopn  24005  fbflim2  24007  flimcf  24012  flimclslem  24014  flffval  24019  flfnei  24021  flftg  24026  cnpflf2  24030  isfcls2  24043  fclsopn  24044  fclsnei  24049  fclscf  24055  fclscmp  24060  fcfval  24063  fcfnei  24065  cnpfcf  24071  tgpmulg2  24124  tmdgsum  24125  tmdgsum2  24126  subgntr  24137  opnsubg  24138  clssubg  24139  clsnsg  24140  cldsubg  24141  snclseqg  24146  tgphaus  24147  qustgpopn  24150  prdstgpd  24155  tsmsgsum  24169  tsmsid  24170  tgptsmscld  24181  mopntop  24472  metdseq0  24898  cnmpopc  24977  ishtpy  25026  om1val  25085  pi1val  25092  csscld  25305  clsocv  25306  relcmpcmet  25374  bcth2  25386  limcres  25944  perfdvf  25961  dvaddbr  25997  dvmulbr  25998  dvmulbrOLD  25999  dvcmulf  26005  dvmptres2  26023  dvmptcmul  26025  dvmptntr  26032  dvcnvlem  26037  lhop2  26077  lhop  26078  dvcnvrelem2  26080  taylthlem1  26438  zartop  33850  neibastop2  36356  neibastop3  36357  topjoin  36360  dissneqlem  37335  istopclsd  42702  dvresntr  45885