Theorem topontop 22800

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4871  ‘cfv 6511  Topctop 22780  TopOnctopon 22797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-topon 22798

This theorem is referenced by:  topontopi  22802  topontopon  22806  toprntopon  22812  toponmax  22813  topgele  22817  istps  22821  en2top  22872  pptbas  22895  toponmre  22980  cldmreon  22981  iscldtop  22982  neiptopreu  23020  resttopon  23048  resttopon2  23055  restlp  23070  restperf  23071  perfopn  23072  ordtopn3  23083  ordtcld1  23084  ordtcld2  23085  ordttop  23087  lmfval  23119  cnfval  23120  cnpfval  23121  tgcn  23139  tgcnp  23140  subbascn  23141  iscnp4  23150  iscncl  23156  cncls2  23160  cncls  23161  cnntr  23162  cncnp  23167  cnindis  23179  lmcls  23189  iscnrm2  23225  ist0-2  23231  ist1-2  23234  ishaus2  23238  hausnei2  23240  isreg2  23264  sscmp  23292  dfconn2  23306  clsconn  23317  conncompcld  23321  1stccnp  23349  locfincf  23418  kgenval  23422  kgenftop  23427  1stckgenlem  23440  kgen2ss  23442  txtopon  23478  pttopon  23483  txcls  23491  ptclsg  23502  dfac14lem  23504  xkoccn  23506  txcnp  23507  ptcnplem  23508  txlm  23535  cnmpt2res  23564  cnmptkp  23567  cnmptk1  23568  cnmpt1k  23569  cnmptkk  23570  cnmptk1p  23572  cnmptk2  23573  xkoinjcn  23574  qtoptopon  23591  qtopcld  23600  qtoprest  23604  qtopcmap  23606  kqval  23613  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  kqtop  23632  pt1hmeo  23693  xpstopnlem1  23696  xkohmeo  23702  neifil  23767  trnei  23779  elflim  23858  flimss1  23860  flimopn  23862  fbflim2  23864  flimcf  23869  flimclslem  23871  flffval  23876  flfnei  23878  flftg  23883  cnpflf2  23887  isfcls2  23900  fclsopn  23901  fclsnei  23906  fclscf  23912  fclscmp  23917  fcfval  23920  fcfnei  23922  cnpfcf  23928  tgpmulg2  23981  tmdgsum  23982  tmdgsum2  23983  subgntr  23994  opnsubg  23995  clssubg  23996  clsnsg  23997  cldsubg  23998  snclseqg  24003  tgphaus  24004  qustgpopn  24007  prdstgpd  24012  tsmsgsum  24026  tsmsid  24027  tgptsmscld  24038  mopntop  24328  metdseq0  24743  cnmpopc  24822  ishtpy  24871  om1val  24930  pi1val  24937  csscld  25149  clsocv  25150  relcmpcmet  25218  bcth2  25230  limcres  25787  perfdvf  25804  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmulf  25848  dvmptres2  25866  dvmptcmul  25868  dvmptntr  25875  dvcnvlem  25880  lhop2  25920  lhop  25921  dvcnvrelem2  25923  taylthlem1  26281  zartop  33866  neibastop2  36349  neibastop3  36350  topjoin  36353  dissneqlem  37328  istopclsd  42688  dvresntr  45916