Theorem topontop 23070

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∪ cuni 4872  ‘cfv 6536  Topctop 23050  TopOnctopon 23067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fv 6544  df-topon 23068

This theorem is referenced by:  topontopi  23072  topontopon  23076  toprntopon  23082  toponmax  23083  topgele  23087  istps  23091  en2top  23142  pptbas  23165  toponmre  23250  cldmreon  23251  iscldtop  23252  neiptopreu  23290  resttopon  23318  resttopon2  23325  restlp  23340  restperf  23341  perfopn  23342  ordtopn3  23353  ordtcld1  23354  ordtcld2  23355  ordttop  23357  lmfval  23389  cnfval  23390  cnpfval  23391  tgcn  23409  tgcnp  23410  subbascn  23411  iscnp4  23420  iscncl  23426  cncls2  23430  cncls  23431  cnntr  23432  cncnp  23437  cnindis  23449  lmcls  23459  iscnrm2  23495  ist0-2  23501  ist1-2  23504  ishaus2  23508  hausnei2  23510  isreg2  23534  sscmp  23562  dfconn2  23576  clsconn  23587  conncompcld  23591  1stccnp  23619  locfincf  23688  kgenval  23692  kgenftop  23697  1stckgenlem  23710  kgen2ss  23712  txtopon  23748  pttopon  23753  txcls  23761  ptclsg  23772  dfac14lem  23774  xkoccn  23776  txcnp  23777  ptcnplem  23778  txlm  23805  cnmpt2res  23834  cnmptkp  23837  cnmptk1  23838  cnmpt1k  23839  cnmptkk  23840  cnmptk1p  23842  cnmptk2  23843  xkoinjcn  23844  qtoptopon  23861  qtopcld  23870  qtoprest  23874  qtopcmap  23876  kqval  23883  regr1lem  23896  kqreglem1  23898  kqreglem2  23899  kqnrmlem1  23900  kqnrmlem2  23901  kqtop  23902  pt1hmeo  23963  xpstopnlem1  23966  xkohmeo  23972  neifil  24037  trnei  24049  elflim  24128  flimss1  24130  flimopn  24132  fbflim2  24134  flimcf  24139  flimclslem  24141  flffval  24146  flfnei  24148  flftg  24153  cnpflf2  24157  isfcls2  24170  fclsopn  24171  fclsnei  24176  fclscf  24182  fclscmp  24187  fcfval  24190  fcfnei  24192  cnpfcf  24198  tgpmulg2  24251  tmdgsum  24252  tmdgsum2  24253  subgntr  24264  opnsubg  24265  clssubg  24266  clsnsg  24267  cldsubg  24268  snclseqg  24273  tgphaus  24274  qustgpopn  24277  prdstgpd  24282  tsmsgsum  24296  tsmsid  24297  tgptsmscld  24308  mopntop  24597  metdseq0  25012  cnmpopc  25087  ishtpy  25131  om1val  25189  pi1val  25196  csscld  25408  clsocv  25409  relcmpcmet  25477  bcth2  25489  limcres  26045  perfdvf  26062  dvaddbr  26097  dvmulbr  26098  dvcmulf  26104  dvmptres2  26121  dvmptcmul  26123  dvmptntr  26130  dvcnvlem  26135  lhop2  26174  lhop  26175  dvcnvrelem2  26177  taylthlem1  26536  zartop  34266  neibastop2  36892  neibastop3  36893  topjoin  36896  dissneqlem  38006  istopclsd  43451  dvresntr  46652