Theorem topontop 22869

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ cuni 4865  ‘cfv 6500  Topctop 22849  TopOnctopon 22866

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-topon 22867

This theorem is referenced by:  topontopi  22871  topontopon  22875  toprntopon  22881  toponmax  22882  topgele  22886  istps  22890  en2top  22941  pptbas  22964  toponmre  23049  cldmreon  23050  iscldtop  23051  neiptopreu  23089  resttopon  23117  resttopon2  23124  restlp  23139  restperf  23140  perfopn  23141  ordtopn3  23152  ordtcld1  23153  ordtcld2  23154  ordttop  23156  lmfval  23188  cnfval  23189  cnpfval  23190  tgcn  23208  tgcnp  23209  subbascn  23210  iscnp4  23219  iscncl  23225  cncls2  23229  cncls  23230  cnntr  23231  cncnp  23236  cnindis  23248  lmcls  23258  iscnrm2  23294  ist0-2  23300  ist1-2  23303  ishaus2  23307  hausnei2  23309  isreg2  23333  sscmp  23361  dfconn2  23375  clsconn  23386  conncompcld  23390  1stccnp  23418  locfincf  23487  kgenval  23491  kgenftop  23496  1stckgenlem  23509  kgen2ss  23511  txtopon  23547  pttopon  23552  txcls  23560  ptclsg  23571  dfac14lem  23573  xkoccn  23575  txcnp  23576  ptcnplem  23577  txlm  23604  cnmpt2res  23633  cnmptkp  23636  cnmptk1  23637  cnmpt1k  23638  cnmptkk  23639  cnmptk1p  23641  cnmptk2  23642  xkoinjcn  23643  qtoptopon  23660  qtopcld  23669  qtoprest  23673  qtopcmap  23675  kqval  23682  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  kqtop  23701  pt1hmeo  23762  xpstopnlem1  23765  xkohmeo  23771  neifil  23836  trnei  23848  elflim  23927  flimss1  23929  flimopn  23931  fbflim2  23933  flimcf  23938  flimclslem  23940  flffval  23945  flfnei  23947  flftg  23952  cnpflf2  23956  isfcls2  23969  fclsopn  23970  fclsnei  23975  fclscf  23981  fclscmp  23986  fcfval  23989  fcfnei  23991  cnpfcf  23997  tgpmulg2  24050  tmdgsum  24051  tmdgsum2  24052  subgntr  24063  opnsubg  24064  clssubg  24065  clsnsg  24066  cldsubg  24067  snclseqg  24072  tgphaus  24073  qustgpopn  24076  prdstgpd  24081  tsmsgsum  24095  tsmsid  24096  tgptsmscld  24107  mopntop  24396  metdseq0  24811  cnmpopc  24890  ishtpy  24939  om1val  24998  pi1val  25005  csscld  25217  clsocv  25218  relcmpcmet  25286  bcth2  25298  limcres  25855  perfdvf  25872  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmulf  25916  dvmptres2  25934  dvmptcmul  25936  dvmptntr  25943  dvcnvlem  25948  lhop2  25988  lhop  25989  dvcnvrelem2  25991  taylthlem1  26349  zartop  34054  neibastop2  36577  neibastop3  36578  topjoin  36581  dissneqlem  37595  istopclsd  43057  dvresntr  46276