Theorem topontop 22973

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

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  ∪ cuni 4865  ‘cfv 6521  Topctop 22953  TopOnctopon 22970

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-nul 5256  ax-pow 5322  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-pw 4557  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-iota 6477  df-fun 6523  df-fv 6529  df-topon 22971

This theorem is referenced by:  topontopi  22975  topontopon  22979  toprntopon  22985  toponmax  22986  topgele  22990  istps  22994  en2top  23045  pptbas  23068  toponmre  23153  cldmreon  23154  iscldtop  23155  neiptopreu  23193  resttopon  23221  resttopon2  23228  restlp  23243  restperf  23244  perfopn  23245  ordtopn3  23256  ordtcld1  23257  ordtcld2  23258  ordttop  23260  lmfval  23292  cnfval  23293  cnpfval  23294  tgcn  23312  tgcnp  23313  subbascn  23314  iscnp4  23323  iscncl  23329  cncls2  23333  cncls  23334  cnntr  23335  cncnp  23340  cnindis  23352  lmcls  23362  iscnrm2  23398  ist0-2  23404  ist1-2  23407  ishaus2  23411  hausnei2  23413  isreg2  23437  sscmp  23465  dfconn2  23479  clsconn  23490  conncompcld  23494  1stccnp  23522  locfincf  23591  kgenval  23595  kgenftop  23600  1stckgenlem  23613  kgen2ss  23615  txtopon  23651  pttopon  23656  txcls  23664  ptclsg  23675  dfac14lem  23677  xkoccn  23679  txcnp  23680  ptcnplem  23681  txlm  23708  cnmpt2res  23737  cnmptkp  23740  cnmptk1  23741  cnmpt1k  23742  cnmptkk  23743  cnmptk1p  23745  cnmptk2  23746  xkoinjcn  23747  qtoptopon  23764  qtopcld  23773  qtoprest  23777  qtopcmap  23779  kqval  23786  regr1lem  23799  kqreglem1  23801  kqreglem2  23802  kqnrmlem1  23803  kqnrmlem2  23804  kqtop  23805  pt1hmeo  23866  xpstopnlem1  23869  xkohmeo  23875  neifil  23940  trnei  23952  elflim  24031  flimss1  24033  flimopn  24035  fbflim2  24037  flimcf  24042  flimclslem  24044  flffval  24049  flfnei  24051  flftg  24056  cnpflf2  24060  isfcls2  24073  fclsopn  24074  fclsnei  24079  fclscf  24085  fclscmp  24090  fcfval  24093  fcfnei  24095  cnpfcf  24101  tgpmulg2  24154  tmdgsum  24155  tmdgsum2  24156  subgntr  24167  opnsubg  24168  clssubg  24169  clsnsg  24170  cldsubg  24171  snclseqg  24176  tgphaus  24177  qustgpopn  24180  prdstgpd  24185  tsmsgsum  24199  tsmsid  24200  tgptsmscld  24211  mopntop  24500  metdseq0  24915  cnmpopc  24990  ishtpy  25034  om1val  25092  pi1val  25099  csscld  25311  clsocv  25312  relcmpcmet  25380  bcth2  25392  limcres  25948  perfdvf  25965  dvaddbr  26000  dvmulbr  26001  dvcmulf  26007  dvmptres2  26024  dvmptcmul  26026  dvmptntr  26033  dvcnvlem  26038  lhop2  26077  lhop  26078  dvcnvrelem2  26080  taylthlem1  26436  zartop  34173  neibastop2  36721  neibastop3  36722  topjoin  36725  dissneqlem  37834  istopclsd  43281  dvresntr  46492