Theorem topontop 23286

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  ∪ cuni 4872  ‘cfv 6566  Topctop 23266  TopOnctopon 23283

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fv 6574  df-topon 23284

This theorem is used by:  topontopi  23288  topontopon  23292  toprntopon  23298  toponmax  23299  topgele  23303  istps  23307  en2top  23358  pptbas  23381  toponmre  23466  cldmreon  23467  iscldtop  23468  neiptopreu  23506  resttopon  23534  resttopon2  23541  restlp  23556  restperf  23557  perfopn  23558  ordtopn3  23569  ordtcld1  23570  ordtcld2  23571  ordttop  23573  lmfval  23605  cnfval  23606  cnpfval  23607  tgcn  23625  tgcnp  23626  subbascn  23627  iscnp4  23636  iscncl  23642  cncls2  23646  cncls  23647  cnntr  23648  cncnp  23653  cnindis  23665  lmcls  23675  iscnrm2  23711  ist0-2  23717  ist1-2  23720  ishaus2  23724  hausnei2  23726  isreg2  23750  sscmp  23778  dfconn2  23792  clsconn  23803  conncompcld  23807  1stccnp  23836  locfincf  23905  kgenval  23909  kgenftop  23914  1stckgenlem  23927  kgen2ss  23929  txtopon  23965  pttopon  23970  txcls  23978  ptclsg  23989  dfac14lem  23991  xkoccn  23993  txcnp  23994  ptcnplem  23995  txlm  24022  cnmpt2res  24051  cnmptkp  24054  cnmptk1  24055  cnmpt1k  24056  cnmptkk  24057  cnmptk1p  24059  cnmptk2  24060  xkoinjcn  24061  qtoptopon  24078  qtopcld  24087  qtoprest  24091  qtopcmap  24093  kqval  24100  regr1lem  24113  kqreglem1  24115  kqreglem2  24116  kqnrmlem1  24117  kqnrmlem2  24118  kqtop  24119  pt1hmeo  24180  xpstopnlem1  24183  xkohmeo  24189  neifil  24254  trnei  24266  elflim  24345  flimss1  24347  flimopn  24349  fbflim2  24351  flimcf  24356  flimclslem  24358  flffval  24363  flfnei  24365  flftg  24370  cnpflf2  24374  isfcls2  24387  fclsopn  24388  fclsnei  24393  fclscf  24399  fclscmp  24404  fcfval  24407  fcfnei  24409  cnpfcf  24415  tgpmulg2  24468  tmdgsum  24469  tmdgsum2  24470  subgntr  24481  opnsubg  24482  clssubg  24483  clsnsg  24484  cldsubg  24485  snclseqg  24490  tgphaus  24491  qustgpopn  24494  prdstgpd  24499  tsmsgsum  24513  tsmsid  24514  tgptsmscld  24525  mopntop  24814  metdseq0  25229  cnmpopc  25304  ishtpy  25348  om1val  25406  pi1val  25413  csscld  25625  clsocv  25626  relcmpcmet  25694  bcth2  25706  limcres  26261  perfdvf  26278  dvaddbr  26313  dvmulbr  26314  dvcmulf  26320  dvmptres2  26337  dvmptcmul  26339  dvmptntr  26346  dvcnvlem  26351  lhop2  26390  lhop  26391  dvcnvrelem2  26393  taylthlem1  26757  zartop  34619  neibastop2  37364  neibastop3  37365  topjoin  37368  dissneqlem  38531  istopclsd  43977  dvresntr  47201