Theorem topontop 22806

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4879  ‘cfv 6519  Topctop 22786  TopOnctopon 22803

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 2702  ax-sep 5259  ax-nul 5269  ax-pow 5328  ax-pr 5395  ax-un 7718

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ral 3047  df-rex 3056  df-rab 3412  df-v 3457  df-dif 3925  df-un 3927  df-in 3929  df-ss 3939  df-nul 4305  df-if 4497  df-pw 4573  df-sn 4598  df-pr 4600  df-op 4604  df-uni 4880  df-br 5116  df-opab 5178  df-mpt 5197  df-id 5541  df-xp 5652  df-rel 5653  df-cnv 5654  df-co 5655  df-dm 5656  df-iota 6472  df-fun 6521  df-fv 6527  df-topon 22804

This theorem is referenced by:  topontopi  22808  topontopon  22812  toprntopon  22818  toponmax  22819  topgele  22823  istps  22827  en2top  22878  pptbas  22901  toponmre  22986  cldmreon  22987  iscldtop  22988  neiptopreu  23026  resttopon  23054  resttopon2  23061  restlp  23076  restperf  23077  perfopn  23078  ordtopn3  23089  ordtcld1  23090  ordtcld2  23091  ordttop  23093  lmfval  23125  cnfval  23126  cnpfval  23127  tgcn  23145  tgcnp  23146  subbascn  23147  iscnp4  23156  iscncl  23162  cncls2  23166  cncls  23167  cnntr  23168  cncnp  23173  cnindis  23185  lmcls  23195  iscnrm2  23231  ist0-2  23237  ist1-2  23240  ishaus2  23244  hausnei2  23246  isreg2  23270  sscmp  23298  dfconn2  23312  clsconn  23323  conncompcld  23327  1stccnp  23355  locfincf  23424  kgenval  23428  kgenftop  23433  1stckgenlem  23446  kgen2ss  23448  txtopon  23484  pttopon  23489  txcls  23497  ptclsg  23508  dfac14lem  23510  xkoccn  23512  txcnp  23513  ptcnplem  23514  txlm  23541  cnmpt2res  23570  cnmptkp  23573  cnmptk1  23574  cnmpt1k  23575  cnmptkk  23576  cnmptk1p  23578  cnmptk2  23579  xkoinjcn  23580  qtoptopon  23597  qtopcld  23606  qtoprest  23610  qtopcmap  23612  kqval  23619  regr1lem  23632  kqreglem1  23634  kqreglem2  23635  kqnrmlem1  23636  kqnrmlem2  23637  kqtop  23638  pt1hmeo  23699  xpstopnlem1  23702  xkohmeo  23708  neifil  23773  trnei  23785  elflim  23864  flimss1  23866  flimopn  23868  fbflim2  23870  flimcf  23875  flimclslem  23877  flffval  23882  flfnei  23884  flftg  23889  cnpflf2  23893  isfcls2  23906  fclsopn  23907  fclsnei  23912  fclscf  23918  fclscmp  23923  fcfval  23926  fcfnei  23928  cnpfcf  23934  tgpmulg2  23987  tmdgsum  23988  tmdgsum2  23989  subgntr  24000  opnsubg  24001  clssubg  24002  clsnsg  24003  cldsubg  24004  snclseqg  24009  tgphaus  24010  qustgpopn  24013  prdstgpd  24018  tsmsgsum  24032  tsmsid  24033  tgptsmscld  24044  mopntop  24334  metdseq0  24749  cnmpopc  24828  ishtpy  24877  om1val  24936  pi1val  24943  csscld  25156  clsocv  25157  relcmpcmet  25225  bcth2  25237  limcres  25794  perfdvf  25811  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmulf  25855  dvmptres2  25873  dvmptcmul  25875  dvmptntr  25882  dvcnvlem  25887  lhop2  25927  lhop  25928  dvcnvrelem2  25930  taylthlem1  26288  zartop  33874  neibastop2  36346  neibastop3  36347  topjoin  36350  dissneqlem  37325  istopclsd  42660  dvresntr  45889