Theorem topontop 22770

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  ∪ cuni 4902  ‘cfv 6537  Topctop 22750  TopOnctopon 22767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ral 3056  df-rex 3065  df-rab 3427  df-v 3470  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-iota 6489  df-fun 6539  df-fv 6545  df-topon 22768

This theorem is referenced by:  topontopi  22772  topontopon  22776  toprntopon  22782  toponmax  22783  topgele  22787  istps  22791  en2top  22843  pptbas  22866  toponmre  22952  cldmreon  22953  iscldtop  22954  neiptopreu  22992  resttopon  23020  resttopon2  23027  restlp  23042  restperf  23043  perfopn  23044  ordtopn3  23055  ordtcld1  23056  ordtcld2  23057  ordttop  23059  lmfval  23091  cnfval  23092  cnpfval  23093  tgcn  23111  tgcnp  23112  subbascn  23113  iscnp4  23122  iscncl  23128  cncls2  23132  cncls  23133  cnntr  23134  cncnp  23139  cnindis  23151  lmcls  23161  iscnrm2  23197  ist0-2  23203  ist1-2  23206  ishaus2  23210  hausnei2  23212  isreg2  23236  sscmp  23264  dfconn2  23278  clsconn  23289  conncompcld  23293  1stccnp  23321  locfincf  23390  kgenval  23394  kgenftop  23399  1stckgenlem  23412  kgen2ss  23414  txtopon  23450  pttopon  23455  txcls  23463  ptclsg  23474  dfac14lem  23476  xkoccn  23478  txcnp  23479  ptcnplem  23480  txlm  23507  cnmpt2res  23536  cnmptkp  23539  cnmptk1  23540  cnmpt1k  23541  cnmptkk  23542  cnmptk1p  23544  cnmptk2  23545  xkoinjcn  23546  qtoptopon  23563  qtopcld  23572  qtoprest  23576  qtopcmap  23578  kqval  23585  regr1lem  23598  kqreglem1  23600  kqreglem2  23601  kqnrmlem1  23602  kqnrmlem2  23603  kqtop  23604  pt1hmeo  23665  xpstopnlem1  23668  xkohmeo  23674  neifil  23739  trnei  23751  elflim  23830  flimss1  23832  flimopn  23834  fbflim2  23836  flimcf  23841  flimclslem  23843  flffval  23848  flfnei  23850  flftg  23855  cnpflf2  23859  isfcls2  23872  fclsopn  23873  fclsnei  23878  fclscf  23884  fclscmp  23889  fcfval  23892  fcfnei  23894  cnpfcf  23900  tgpmulg2  23953  tmdgsum  23954  tmdgsum2  23955  subgntr  23966  opnsubg  23967  clssubg  23968  clsnsg  23969  cldsubg  23970  snclseqg  23975  tgphaus  23976  qustgpopn  23979  prdstgpd  23984  tsmsgsum  23998  tsmsid  23999  tgptsmscld  24010  mopntop  24301  metdseq0  24725  cnmpopc  24804  ishtpy  24853  om1val  24912  pi1val  24919  csscld  25132  clsocv  25133  relcmpcmet  25201  bcth2  25213  limcres  25770  perfdvf  25787  dvaddbr  25823  dvmulbr  25824  dvmulbrOLD  25825  dvcmulf  25831  dvmptres2  25849  dvmptcmul  25851  dvmptntr  25858  dvcnvlem  25863  lhop2  25903  lhop  25904  dvcnvrelem2  25906  taylthlem1  26263  zartop  33386  neibastop2  35754  neibastop3  35755  topjoin  35758  dissneqlem  36728  istopclsd  42013  dvresntr  45203