Theorem topontop 22160

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ∪ cuni 4851  ‘cfv 6473  Topctop 22140  TopOnctopon 22157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-br 5090  df-opab 5152  df-mpt 5173  df-id 5512  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6425  df-fun 6475  df-fv 6481  df-topon 22158

This theorem is referenced by:  topontopi  22162  topontopon  22166  toprntopon  22172  toponmax  22173  topgele  22177  istps  22181  en2top  22233  pptbas  22256  toponmre  22342  cldmreon  22343  iscldtop  22344  neiptopreu  22382  resttopon  22410  resttopon2  22417  restlp  22432  restperf  22433  perfopn  22434  ordtopn3  22445  ordtcld1  22446  ordtcld2  22447  ordttop  22449  lmfval  22481  cnfval  22482  cnpfval  22483  tgcn  22501  tgcnp  22502  subbascn  22503  iscnp4  22512  iscncl  22518  cncls2  22522  cncls  22523  cnntr  22524  cncnp  22529  cnindis  22541  lmcls  22551  iscnrm2  22587  ist0-2  22593  ist1-2  22596  ishaus2  22600  hausnei2  22602  isreg2  22626  sscmp  22654  dfconn2  22668  clsconn  22679  conncompcld  22683  1stccnp  22711  locfincf  22780  kgenval  22784  kgenftop  22789  1stckgenlem  22802  kgen2ss  22804  txtopon  22840  pttopon  22845  txcls  22853  ptclsg  22864  dfac14lem  22866  xkoccn  22868  txcnp  22869  ptcnplem  22870  txlm  22897  cnmpt2res  22926  cnmptkp  22929  cnmptk1  22930  cnmpt1k  22931  cnmptkk  22932  cnmptk1p  22934  cnmptk2  22935  xkoinjcn  22936  qtoptopon  22953  qtopcld  22962  qtoprest  22966  qtopcmap  22968  kqval  22975  regr1lem  22988  kqreglem1  22990  kqreglem2  22991  kqnrmlem1  22992  kqnrmlem2  22993  kqtop  22994  pt1hmeo  23055  xpstopnlem1  23058  xkohmeo  23064  neifil  23129  trnei  23141  elflim  23220  flimss1  23222  flimopn  23224  fbflim2  23226  flimcf  23231  flimclslem  23233  flffval  23238  flfnei  23240  flftg  23245  cnpflf2  23249  isfcls2  23262  fclsopn  23263  fclsnei  23268  fclscf  23274  fclscmp  23279  fcfval  23282  fcfnei  23284  cnpfcf  23290  tgpmulg2  23343  tmdgsum  23344  tmdgsum2  23345  subgntr  23356  opnsubg  23357  clssubg  23358  clsnsg  23359  cldsubg  23360  snclseqg  23365  tgphaus  23366  qustgpopn  23369  prdstgpd  23374  tsmsgsum  23388  tsmsid  23389  tgptsmscld  23400  mopntop  23691  metdseq0  24115  cnmpopc  24189  ishtpy  24233  om1val  24291  pi1val  24298  csscld  24511  clsocv  24512  relcmpcmet  24580  bcth2  24592  limcres  25148  perfdvf  25165  dvaddbr  25200  dvmulbr  25201  dvcmulf  25207  dvmptres2  25224  dvmptcmul  25226  dvmptntr  25233  dvcnvlem  25238  lhop2  25277  lhop  25278  dvcnvrelem2  25280  taylthlem1  25630  zartop  32065  neibastop2  34641  neibastop3  34642  topjoin  34645  dissneqlem  35609  istopclsd  40772  dvresntr  43784