Theorem topontop 23243

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2146  ∪ cuni 4869  ‘cfv 6546  Topctop 23223  TopOnctopon 23240

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6500  df-fun 6548  df-fv 6554  df-topon 23241

This theorem is used by:  topontopi  23245  topontopon  23249  toprntopon  23255  toponmax  23256  topgele  23260  istps  23264  en2top  23315  pptbas  23338  toponmre  23423  cldmreon  23424  iscldtop  23425  neiptopreu  23463  resttopon  23491  resttopon2  23498  restlp  23513  restperf  23514  perfopn  23515  ordtopn3  23526  ordtcld1  23527  ordtcld2  23528  ordttop  23530  lmfval  23562  cnfval  23563  cnpfval  23564  tgcn  23582  tgcnp  23583  subbascn  23584  iscnp4  23593  iscncl  23599  cncls2  23603  cncls  23604  cnntr  23605  cncnp  23610  cnindis  23622  lmcls  23632  iscnrm2  23668  ist0-2  23674  ist1-2  23677  ishaus2  23681  hausnei2  23683  isreg2  23707  sscmp  23735  dfconn2  23749  clsconn  23760  conncompcld  23764  1stccnp  23793  locfincf  23862  kgenval  23866  kgenftop  23871  1stckgenlem  23884  kgen2ss  23886  txtopon  23922  pttopon  23927  txcls  23935  ptclsg  23946  dfac14lem  23948  xkoccn  23950  txcnp  23951  ptcnplem  23952  txlm  23979  cnmpt2res  24008  cnmptkp  24011  cnmptk1  24012  cnmpt1k  24013  cnmptkk  24014  cnmptk1p  24016  cnmptk2  24017  xkoinjcn  24018  qtoptopon  24035  qtopcld  24044  qtoprest  24048  qtopcmap  24050  kqval  24057  regr1lem  24070  kqreglem1  24072  kqreglem2  24073  kqnrmlem1  24074  kqnrmlem2  24075  kqtop  24076  pt1hmeo  24137  xpstopnlem1  24140  xkohmeo  24146  neifil  24211  trnei  24223  elflim  24302  flimss1  24304  flimopn  24306  fbflim2  24308  flimcf  24313  flimclslem  24315  flffval  24320  flfnei  24322  flftg  24327  cnpflf2  24331  isfcls2  24344  fclsopn  24345  fclsnei  24350  fclscf  24356  fclscmp  24361  fcfval  24364  fcfnei  24366  cnpfcf  24372  tgpmulg2  24425  tmdgsum  24426  tmdgsum2  24427  subgntr  24438  opnsubg  24439  clssubg  24440  clsnsg  24441  cldsubg  24442  snclseqg  24447  tgphaus  24448  qustgpopn  24451  prdstgpd  24456  tsmsgsum  24470  tsmsid  24471  tgptsmscld  24482  mopntop  24771  metdseq0  25186  cnmpopc  25261  ishtpy  25305  om1val  25363  pi1val  25370  csscld  25582  clsocv  25583  relcmpcmet  25651  bcth2  25663  limcres  26218  perfdvf  26235  dvaddbr  26270  dvmulbr  26271  dvcmulf  26277  dvmptres2  26294  dvmptcmul  26296  dvmptntr  26303  dvcnvlem  26308  lhop2  26347  lhop  26348  dvcnvrelem2  26350  taylthlem1  26712  zartop  34561  neibastop2  37276  neibastop3  37277  topjoin  37280  dissneqlem  38403  istopclsd  43851  dvresntr  47067