Theorem topontop 20935

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

Syntax hints:   → wi 4   = wceq 1637   ∈ wcel 2157  ∪ cuni 4637  ‘cfv 6104  Topctop 20915  TopOnctopon 20932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-sbc 3641  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-opab 4914  df-mpt 4931  df-id 5226  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-iota 6067  df-fun 6106  df-fv 6112  df-topon 20933

This theorem is referenced by:  topontopi  20937  topontopon  20941  toprntopon  20947  toponmax  20948  topgele  20952  istps  20956  en2top  21007  pptbas  21030  toponmre  21115  cldmreon  21116  iscldtop  21117  neiptopreu  21155  resttopon  21183  resttopon2  21190  restlp  21205  restperf  21206  perfopn  21207  ordtopn3  21218  ordtcld1  21219  ordtcld2  21220  ordttop  21222  lmfval  21254  cnfval  21255  cnpfval  21256  tgcn  21274  tgcnp  21275  subbascn  21276  iscnp4  21285  iscncl  21291  cncls2  21295  cncls  21296  cnntr  21297  cncnp  21302  cnindis  21314  lmcls  21324  iscnrm2  21360  ist0-2  21366  ist1-2  21369  ishaus2  21373  hausnei2  21375  isreg2  21399  sscmp  21426  dfconn2  21440  clsconn  21451  conncompcld  21455  1stccnp  21483  locfincf  21552  kgenval  21556  kgenftop  21561  1stckgenlem  21574  kgen2ss  21576  txtopon  21612  pttopon  21617  txcls  21625  ptclsg  21636  dfac14lem  21638  xkoccn  21640  txcnp  21641  ptcnplem  21642  txlm  21669  cnmpt2res  21698  cnmptkp  21701  cnmptk1  21702  cnmpt1k  21703  cnmptkk  21704  cnmptk1p  21706  cnmptk2  21707  xkoinjcn  21708  qtoptopon  21725  qtopcld  21734  qtoprest  21738  qtopcmap  21740  kqval  21747  regr1lem  21760  kqreglem1  21762  kqreglem2  21763  kqnrmlem1  21764  kqnrmlem2  21765  kqtop  21766  pt1hmeo  21827  xpstopnlem1  21830  xkohmeo  21836  neifil  21901  trnei  21913  elflim  21992  flimss1  21994  flimopn  21996  fbflim2  21998  flimcf  22003  flimclslem  22005  flffval  22010  flfnei  22012  flftg  22017  cnpflf2  22021  isfcls2  22034  fclsopn  22035  fclsnei  22040  fclscf  22046  fclscmp  22051  fcfval  22054  fcfnei  22056  cnpfcf  22062  tgpmulg2  22115  tmdgsum  22116  tmdgsum2  22117  subgntr  22127  opnsubg  22128  clssubg  22129  clsnsg  22130  cldsubg  22131  snclseqg  22136  tgphaus  22137  qustgpopn  22140  prdstgpd  22145  tsmsgsum  22159  tsmsid  22160  tgptsmscld  22171  mopntop  22462  metdseq0  22874  cnmpt2pc  22944  ishtpy  22988  om1val  23046  pi1val  23053  csscld  23264  clsocv  23265  relcmpcmet  23332  bcth2  23344  limcres  23870  perfdvf  23887  dvaddbr  23921  dvmulbr  23922  dvcmulf  23928  dvmptres2  23945  dvmptcmul  23947  dvmptntr  23954  dvcnvlem  23959  lhop2  23998  lhop  23999  dvcnvrelem2  24001  taylthlem1  24347  neibastop2  32682  neibastop3  32683  topjoin  32686  dissneqlem  33506  istopclsd  37766  dvresntr  40613