Theorem topontop 23122

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  ∪ cuni 4874  ‘cfv 6540  Topctop 23102  TopOnctopon 23119

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fv 6548  df-topon 23120

This theorem is used by:  topontopi  23124  topontopon  23128  toprntopon  23134  toponmax  23135  topgele  23139  istps  23143  en2top  23194  pptbas  23217  toponmre  23302  cldmreon  23303  iscldtop  23304  neiptopreu  23342  resttopon  23370  resttopon2  23377  restlp  23392  restperf  23393  perfopn  23394  ordtopn3  23405  ordtcld1  23406  ordtcld2  23407  ordttop  23409  lmfval  23441  cnfval  23442  cnpfval  23443  tgcn  23461  tgcnp  23462  subbascn  23463  iscnp4  23472  iscncl  23478  cncls2  23482  cncls  23483  cnntr  23484  cncnp  23489  cnindis  23501  lmcls  23511  iscnrm2  23547  ist0-2  23553  ist1-2  23556  ishaus2  23560  hausnei2  23562  isreg2  23586  sscmp  23614  dfconn2  23628  clsconn  23639  conncompcld  23643  1stccnp  23672  locfincf  23741  kgenval  23745  kgenftop  23750  1stckgenlem  23763  kgen2ss  23765  txtopon  23801  pttopon  23806  txcls  23814  ptclsg  23825  dfac14lem  23827  xkoccn  23829  txcnp  23830  ptcnplem  23831  txlm  23858  cnmpt2res  23887  cnmptkp  23890  cnmptk1  23891  cnmpt1k  23892  cnmptkk  23893  cnmptk1p  23895  cnmptk2  23896  xkoinjcn  23897  qtoptopon  23914  qtopcld  23923  qtoprest  23927  qtopcmap  23929  kqval  23936  regr1lem  23949  kqreglem1  23951  kqreglem2  23952  kqnrmlem1  23953  kqnrmlem2  23954  kqtop  23955  pt1hmeo  24016  xpstopnlem1  24019  xkohmeo  24025  neifil  24090  trnei  24102  elflim  24181  flimss1  24183  flimopn  24185  fbflim2  24187  flimcf  24192  flimclslem  24194  flffval  24199  flfnei  24201  flftg  24206  cnpflf2  24210  isfcls2  24223  fclsopn  24224  fclsnei  24229  fclscf  24235  fclscmp  24240  fcfval  24243  fcfnei  24245  cnpfcf  24251  tgpmulg2  24304  tmdgsum  24305  tmdgsum2  24306  subgntr  24317  opnsubg  24318  clssubg  24319  clsnsg  24320  cldsubg  24321  snclseqg  24326  tgphaus  24327  qustgpopn  24330  prdstgpd  24335  tsmsgsum  24349  tsmsid  24350  tgptsmscld  24361  mopntop  24650  metdseq0  25065  cnmpopc  25140  ishtpy  25184  om1val  25242  pi1val  25249  csscld  25461  clsocv  25462  relcmpcmet  25530  bcth2  25542  limcres  26098  perfdvf  26115  dvaddbr  26150  dvmulbr  26151  dvcmulf  26157  dvmptres2  26174  dvmptcmul  26176  dvmptntr  26183  dvcnvlem  26188  lhop2  26227  lhop  26228  dvcnvrelem2  26230  taylthlem1  26589  zartop  34332  neibastop2  36931  neibastop3  36932  topjoin  36935  dissneqlem  38045  istopclsd  43491  dvresntr  46692