Theorem topontop 22833

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4867  ‘cfv 6499  Topctop 22813  TopOnctopon 22830

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6452  df-fun 6501  df-fv 6507  df-topon 22831

This theorem is referenced by:  topontopi  22835  topontopon  22839  toprntopon  22845  toponmax  22846  topgele  22850  istps  22854  en2top  22905  pptbas  22928  toponmre  23013  cldmreon  23014  iscldtop  23015  neiptopreu  23053  resttopon  23081  resttopon2  23088  restlp  23103  restperf  23104  perfopn  23105  ordtopn3  23116  ordtcld1  23117  ordtcld2  23118  ordttop  23120  lmfval  23152  cnfval  23153  cnpfval  23154  tgcn  23172  tgcnp  23173  subbascn  23174  iscnp4  23183  iscncl  23189  cncls2  23193  cncls  23194  cnntr  23195  cncnp  23200  cnindis  23212  lmcls  23222  iscnrm2  23258  ist0-2  23264  ist1-2  23267  ishaus2  23271  hausnei2  23273  isreg2  23297  sscmp  23325  dfconn2  23339  clsconn  23350  conncompcld  23354  1stccnp  23382  locfincf  23451  kgenval  23455  kgenftop  23460  1stckgenlem  23473  kgen2ss  23475  txtopon  23511  pttopon  23516  txcls  23524  ptclsg  23535  dfac14lem  23537  xkoccn  23539  txcnp  23540  ptcnplem  23541  txlm  23568  cnmpt2res  23597  cnmptkp  23600  cnmptk1  23601  cnmpt1k  23602  cnmptkk  23603  cnmptk1p  23605  cnmptk2  23606  xkoinjcn  23607  qtoptopon  23624  qtopcld  23633  qtoprest  23637  qtopcmap  23639  kqval  23646  regr1lem  23659  kqreglem1  23661  kqreglem2  23662  kqnrmlem1  23663  kqnrmlem2  23664  kqtop  23665  pt1hmeo  23726  xpstopnlem1  23729  xkohmeo  23735  neifil  23800  trnei  23812  elflim  23891  flimss1  23893  flimopn  23895  fbflim2  23897  flimcf  23902  flimclslem  23904  flffval  23909  flfnei  23911  flftg  23916  cnpflf2  23920  isfcls2  23933  fclsopn  23934  fclsnei  23939  fclscf  23945  fclscmp  23950  fcfval  23953  fcfnei  23955  cnpfcf  23961  tgpmulg2  24014  tmdgsum  24015  tmdgsum2  24016  subgntr  24027  opnsubg  24028  clssubg  24029  clsnsg  24030  cldsubg  24031  snclseqg  24036  tgphaus  24037  qustgpopn  24040  prdstgpd  24045  tsmsgsum  24059  tsmsid  24060  tgptsmscld  24071  mopntop  24361  metdseq0  24776  cnmpopc  24855  ishtpy  24904  om1val  24963  pi1val  24970  csscld  25182  clsocv  25183  relcmpcmet  25251  bcth2  25263  limcres  25820  perfdvf  25837  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcmulf  25881  dvmptres2  25899  dvmptcmul  25901  dvmptntr  25908  dvcnvlem  25913  lhop2  25953  lhop  25954  dvcnvrelem2  25956  taylthlem1  26314  zartop  33859  neibastop2  36342  neibastop3  36343  topjoin  36346  dissneqlem  37321  istopclsd  42681  dvresntr  45909