Theorem topontop 22886

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2107  ∪ cuni 4889  ‘cfv 6542  Topctop 22866  TopOnctopon 22883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-iota 6495  df-fun 6544  df-fv 6550  df-topon 22884

This theorem is referenced by:  topontopi  22888  topontopon  22892  toprntopon  22898  toponmax  22899  topgele  22903  istps  22907  en2top  22958  pptbas  22981  toponmre  23066  cldmreon  23067  iscldtop  23068  neiptopreu  23106  resttopon  23134  resttopon2  23141  restlp  23156  restperf  23157  perfopn  23158  ordtopn3  23169  ordtcld1  23170  ordtcld2  23171  ordttop  23173  lmfval  23205  cnfval  23206  cnpfval  23207  tgcn  23225  tgcnp  23226  subbascn  23227  iscnp4  23236  iscncl  23242  cncls2  23246  cncls  23247  cnntr  23248  cncnp  23253  cnindis  23265  lmcls  23275  iscnrm2  23311  ist0-2  23317  ist1-2  23320  ishaus2  23324  hausnei2  23326  isreg2  23350  sscmp  23378  dfconn2  23392  clsconn  23403  conncompcld  23407  1stccnp  23435  locfincf  23504  kgenval  23508  kgenftop  23513  1stckgenlem  23526  kgen2ss  23528  txtopon  23564  pttopon  23569  txcls  23577  ptclsg  23588  dfac14lem  23590  xkoccn  23592  txcnp  23593  ptcnplem  23594  txlm  23621  cnmpt2res  23650  cnmptkp  23653  cnmptk1  23654  cnmpt1k  23655  cnmptkk  23656  cnmptk1p  23658  cnmptk2  23659  xkoinjcn  23660  qtoptopon  23677  qtopcld  23686  qtoprest  23690  qtopcmap  23692  kqval  23699  regr1lem  23712  kqreglem1  23714  kqreglem2  23715  kqnrmlem1  23716  kqnrmlem2  23717  kqtop  23718  pt1hmeo  23779  xpstopnlem1  23782  xkohmeo  23788  neifil  23853  trnei  23865  elflim  23944  flimss1  23946  flimopn  23948  fbflim2  23950  flimcf  23955  flimclslem  23957  flffval  23962  flfnei  23964  flftg  23969  cnpflf2  23973  isfcls2  23986  fclsopn  23987  fclsnei  23992  fclscf  23998  fclscmp  24003  fcfval  24006  fcfnei  24008  cnpfcf  24014  tgpmulg2  24067  tmdgsum  24068  tmdgsum2  24069  subgntr  24080  opnsubg  24081  clssubg  24082  clsnsg  24083  cldsubg  24084  snclseqg  24089  tgphaus  24090  qustgpopn  24093  prdstgpd  24098  tsmsgsum  24112  tsmsid  24113  tgptsmscld  24124  mopntop  24414  metdseq0  24831  cnmpopc  24910  ishtpy  24959  om1val  25018  pi1val  25025  csscld  25238  clsocv  25239  relcmpcmet  25307  bcth2  25319  limcres  25876  perfdvf  25893  dvaddbr  25929  dvmulbr  25930  dvmulbrOLD  25931  dvcmulf  25937  dvmptres2  25955  dvmptcmul  25957  dvmptntr  25964  dvcnvlem  25969  lhop2  26009  lhop  26010  dvcnvrelem2  26012  taylthlem1  26370  zartop  33816  neibastop2  36303  neibastop3  36304  topjoin  36307  dissneqlem  37282  istopclsd  42656  dvresntr  45878