Theorem topontop 23231

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6538  Topctop 23211  TopOnctopon 23228

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fv 6546  df-topon 23229

This theorem is used by:  topontopi  23233  topontopon  23237  toprntopon  23243  toponmax  23244  topgele  23248  istps  23252  en2top  23303  pptbas  23326  toponmre  23411  cldmreon  23412  iscldtop  23413  neiptopreu  23451  resttopon  23479  resttopon2  23486  restlp  23501  restperf  23502  perfopn  23503  ordtopn3  23514  ordtcld1  23515  ordtcld2  23516  ordttop  23518  lmfval  23550  cnfval  23551  cnpfval  23552  tgcn  23570  tgcnp  23571  subbascn  23572  iscnp4  23581  iscncl  23587  cncls2  23591  cncls  23592  cnntr  23593  cncnp  23598  cnindis  23610  lmcls  23620  iscnrm2  23656  ist0-2  23662  ist1-2  23665  ishaus2  23669  hausnei2  23671  isreg2  23695  sscmp  23723  dfconn2  23737  clsconn  23748  conncompcld  23752  1stccnp  23781  locfincf  23850  kgenval  23854  kgenftop  23859  1stckgenlem  23872  kgen2ss  23874  txtopon  23910  pttopon  23915  txcls  23923  ptclsg  23934  dfac14lem  23936  xkoccn  23938  txcnp  23939  ptcnplem  23940  txlm  23967  cnmpt2res  23996  cnmptkp  23999  cnmptk1  24000  cnmpt1k  24001  cnmptkk  24002  cnmptk1p  24004  cnmptk2  24005  xkoinjcn  24006  qtoptopon  24023  qtopcld  24032  qtoprest  24036  qtopcmap  24038  kqval  24045  regr1lem  24058  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  kqtop  24064  pt1hmeo  24125  xpstopnlem1  24128  xkohmeo  24134  neifil  24199  trnei  24211  elflim  24290  flimss1  24292  flimopn  24294  fbflim2  24296  flimcf  24301  flimclslem  24303  flffval  24308  flfnei  24310  flftg  24315  cnpflf2  24319  isfcls2  24332  fclsopn  24333  fclsnei  24338  fclscf  24344  fclscmp  24349  fcfval  24352  fcfnei  24354  cnpfcf  24360  tgpmulg2  24413  tmdgsum  24414  tmdgsum2  24415  subgntr  24426  opnsubg  24427  clssubg  24428  clsnsg  24429  cldsubg  24430  snclseqg  24435  tgphaus  24436  qustgpopn  24439  prdstgpd  24444  tsmsgsum  24458  tsmsid  24459  tgptsmscld  24470  mopntop  24759  metdseq0  25174  cnmpopc  25249  ishtpy  25293  om1val  25351  pi1val  25358  csscld  25570  clsocv  25571  relcmpcmet  25639  bcth2  25651  limcres  26206  perfdvf  26223  dvaddbr  26258  dvmulbr  26259  dvcmulf  26265  dvmptres2  26282  dvmptcmul  26284  dvmptntr  26291  dvcnvlem  26296  lhop2  26335  lhop  26336  dvcnvrelem2  26338  taylthlem1  26700  zartop  34508  neibastop2  37149  neibastop3  37150  topjoin  37153  dissneqlem  38263  istopclsd  43710  dvresntr  46927