Theorem topontop 22896

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∪ cuni 4838  ‘cfv 6485  Topctop 22876  TopOnctopon 22893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fv 6493  df-topon 22894

This theorem is referenced by:  topontopi  22898  topontopon  22902  toprntopon  22908  toponmax  22909  topgele  22913  istps  22917  en2top  22968  pptbas  22991  toponmre  23076  cldmreon  23077  iscldtop  23078  neiptopreu  23116  resttopon  23144  resttopon2  23151  restlp  23166  restperf  23167  perfopn  23168  ordtopn3  23179  ordtcld1  23180  ordtcld2  23181  ordttop  23183  lmfval  23215  cnfval  23216  cnpfval  23217  tgcn  23235  tgcnp  23236  subbascn  23237  iscnp4  23246  iscncl  23252  cncls2  23256  cncls  23257  cnntr  23258  cncnp  23263  cnindis  23275  lmcls  23285  iscnrm2  23321  ist0-2  23327  ist1-2  23330  ishaus2  23334  hausnei2  23336  isreg2  23360  sscmp  23388  dfconn2  23402  clsconn  23413  conncompcld  23417  1stccnp  23445  locfincf  23514  kgenval  23518  kgenftop  23523  1stckgenlem  23536  kgen2ss  23538  txtopon  23574  pttopon  23579  txcls  23587  ptclsg  23598  dfac14lem  23600  xkoccn  23602  txcnp  23603  ptcnplem  23604  txlm  23631  cnmpt2res  23660  cnmptkp  23663  cnmptk1  23664  cnmpt1k  23665  cnmptkk  23666  cnmptk1p  23668  cnmptk2  23669  xkoinjcn  23670  qtoptopon  23687  qtopcld  23696  qtoprest  23700  qtopcmap  23702  kqval  23709  regr1lem  23722  kqreglem1  23724  kqreglem2  23725  kqnrmlem1  23726  kqnrmlem2  23727  kqtop  23728  pt1hmeo  23789  xpstopnlem1  23792  xkohmeo  23798  neifil  23863  trnei  23875  elflim  23954  flimss1  23956  flimopn  23958  fbflim2  23960  flimcf  23965  flimclslem  23967  flffval  23972  flfnei  23974  flftg  23979  cnpflf2  23983  isfcls2  23996  fclsopn  23997  fclsnei  24002  fclscf  24008  fclscmp  24013  fcfval  24016  fcfnei  24018  cnpfcf  24024  tgpmulg2  24077  tmdgsum  24078  tmdgsum2  24079  subgntr  24090  opnsubg  24091  clssubg  24092  clsnsg  24093  cldsubg  24094  snclseqg  24099  tgphaus  24100  qustgpopn  24103  prdstgpd  24108  tsmsgsum  24122  tsmsid  24123  tgptsmscld  24134  mopntop  24423  metdseq0  24838  cnmpopc  24913  ishtpy  24957  om1val  25015  pi1val  25022  csscld  25234  clsocv  25235  relcmpcmet  25303  bcth2  25315  limcres  25871  perfdvf  25888  dvaddbr  25923  dvmulbr  25924  dvcmulf  25930  dvmptres2  25947  dvmptcmul  25949  dvmptntr  25956  dvcnvlem  25961  lhop2  26000  lhop  26001  dvcnvrelem2  26003  taylthlem1  26356  zartop  34060  neibastop2  36589  neibastop3  36590  topjoin  36593  dissneqlem  37702  istopclsd  43149  dvresntr  46361