Theorem topontop 20938

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

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145  ∪ cuni 4574  ‘cfv 6031  Topctop 20918  TopOnctopon 20935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-topon 20936

This theorem is referenced by:  topontopi  20940  topontopon  20944  toprntopon  20950  toponmax  20951  topgele  20955  istps  20959  en2top  21010  pptbas  21033  toponmre  21118  cldmreon  21119  iscldtop  21120  neiptopreu  21158  resttopon  21186  resttopon2  21193  restlp  21208  restperf  21209  perfopn  21210  ordtopn3  21221  ordtcld1  21222  ordtcld2  21223  ordttop  21225  lmfval  21257  cnfval  21258  cnpfval  21259  tgcn  21277  tgcnp  21278  subbascn  21279  iscnp4  21288  iscncl  21294  cncls2  21298  cncls  21299  cnntr  21300  cncnp  21305  cnindis  21317  lmcls  21327  iscnrm2  21363  ist0-2  21369  ist1-2  21372  ishaus2  21376  hausnei2  21378  isreg2  21402  sscmp  21429  dfconn2  21443  clsconn  21454  conncompcld  21458  1stccnp  21486  locfincf  21555  kgenval  21559  kgenftop  21564  1stckgenlem  21577  kgen2ss  21579  txtopon  21615  pttopon  21620  txcls  21628  ptclsg  21639  dfac14lem  21641  xkoccn  21643  txcnp  21644  ptcnplem  21645  txlm  21672  cnmpt2res  21701  cnmptkp  21704  cnmptk1  21705  cnmpt1k  21706  cnmptkk  21707  cnmptk1p  21709  cnmptk2  21710  xkoinjcn  21711  qtoptopon  21728  qtopcld  21737  qtoprest  21741  qtopcmap  21743  kqval  21750  regr1lem  21763  kqreglem1  21765  kqreglem2  21766  kqnrmlem1  21767  kqnrmlem2  21768  kqtop  21769  pt1hmeo  21830  xpstopnlem1  21833  xkohmeo  21839  neifil  21904  trnei  21916  elflim  21995  flimss1  21997  flimopn  21999  fbflim2  22001  flimcf  22006  flimclslem  22008  flffval  22013  flfnei  22015  flftg  22020  cnpflf2  22024  isfcls2  22037  fclsopn  22038  fclsnei  22043  fclscf  22049  fclscmp  22054  fcfval  22057  fcfnei  22059  cnpfcf  22065  tgpmulg2  22118  tmdgsum  22119  tmdgsum2  22120  subgntr  22130  opnsubg  22131  clssubg  22132  clsnsg  22133  cldsubg  22134  snclseqg  22139  tgphaus  22140  qustgpopn  22143  prdstgpd  22148  tsmsgsum  22162  tsmsid  22163  tgptsmscld  22174  mopntop  22465  metdseq0  22877  cnmpt2pc  22947  ishtpy  22991  om1val  23049  pi1val  23056  csscld  23267  clsocv  23268  relcmpcmet  23334  bcth2  23346  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  32693  neibastop3  32694  topjoin  32697  dissneqlem  33524  istopclsd  37789  dvresntr  40650