Theorem topontop 22940

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  ∪ cuni 4931  ‘cfv 6573  Topctop 22920  TopOnctopon 22937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fv 6581  df-topon 22938

This theorem is referenced by:  topontopi  22942  topontopon  22946  toprntopon  22952  toponmax  22953  topgele  22957  istps  22961  en2top  23013  pptbas  23036  toponmre  23122  cldmreon  23123  iscldtop  23124  neiptopreu  23162  resttopon  23190  resttopon2  23197  restlp  23212  restperf  23213  perfopn  23214  ordtopn3  23225  ordtcld1  23226  ordtcld2  23227  ordttop  23229  lmfval  23261  cnfval  23262  cnpfval  23263  tgcn  23281  tgcnp  23282  subbascn  23283  iscnp4  23292  iscncl  23298  cncls2  23302  cncls  23303  cnntr  23304  cncnp  23309  cnindis  23321  lmcls  23331  iscnrm2  23367  ist0-2  23373  ist1-2  23376  ishaus2  23380  hausnei2  23382  isreg2  23406  sscmp  23434  dfconn2  23448  clsconn  23459  conncompcld  23463  1stccnp  23491  locfincf  23560  kgenval  23564  kgenftop  23569  1stckgenlem  23582  kgen2ss  23584  txtopon  23620  pttopon  23625  txcls  23633  ptclsg  23644  dfac14lem  23646  xkoccn  23648  txcnp  23649  ptcnplem  23650  txlm  23677  cnmpt2res  23706  cnmptkp  23709  cnmptk1  23710  cnmpt1k  23711  cnmptkk  23712  cnmptk1p  23714  cnmptk2  23715  xkoinjcn  23716  qtoptopon  23733  qtopcld  23742  qtoprest  23746  qtopcmap  23748  kqval  23755  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  kqtop  23774  pt1hmeo  23835  xpstopnlem1  23838  xkohmeo  23844  neifil  23909  trnei  23921  elflim  24000  flimss1  24002  flimopn  24004  fbflim2  24006  flimcf  24011  flimclslem  24013  flffval  24018  flfnei  24020  flftg  24025  cnpflf2  24029  isfcls2  24042  fclsopn  24043  fclsnei  24048  fclscf  24054  fclscmp  24059  fcfval  24062  fcfnei  24064  cnpfcf  24070  tgpmulg2  24123  tmdgsum  24124  tmdgsum2  24125  subgntr  24136  opnsubg  24137  clssubg  24138  clsnsg  24139  cldsubg  24140  snclseqg  24145  tgphaus  24146  qustgpopn  24149  prdstgpd  24154  tsmsgsum  24168  tsmsid  24169  tgptsmscld  24180  mopntop  24471  metdseq0  24895  cnmpopc  24974  ishtpy  25023  om1val  25082  pi1val  25089  csscld  25302  clsocv  25303  relcmpcmet  25371  bcth2  25383  limcres  25941  perfdvf  25958  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmulf  26002  dvmptres2  26020  dvmptcmul  26022  dvmptntr  26029  dvcnvlem  26034  lhop2  26074  lhop  26075  dvcnvrelem2  26077  taylthlem1  26433  zartop  33822  neibastop2  36327  neibastop3  36328  topjoin  36331  dissneqlem  37306  istopclsd  42656  dvresntr  45839