Theorem topontop 22828

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∪ cuni 4856  ‘cfv 6481  Topctop 22808  TopOnctopon 22825

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6437  df-fun 6483  df-fv 6489  df-topon 22826

This theorem is referenced by:  topontopi  22830  topontopon  22834  toprntopon  22840  toponmax  22841  topgele  22845  istps  22849  en2top  22900  pptbas  22923  toponmre  23008  cldmreon  23009  iscldtop  23010  neiptopreu  23048  resttopon  23076  resttopon2  23083  restlp  23098  restperf  23099  perfopn  23100  ordtopn3  23111  ordtcld1  23112  ordtcld2  23113  ordttop  23115  lmfval  23147  cnfval  23148  cnpfval  23149  tgcn  23167  tgcnp  23168  subbascn  23169  iscnp4  23178  iscncl  23184  cncls2  23188  cncls  23189  cnntr  23190  cncnp  23195  cnindis  23207  lmcls  23217  iscnrm2  23253  ist0-2  23259  ist1-2  23262  ishaus2  23266  hausnei2  23268  isreg2  23292  sscmp  23320  dfconn2  23334  clsconn  23345  conncompcld  23349  1stccnp  23377  locfincf  23446  kgenval  23450  kgenftop  23455  1stckgenlem  23468  kgen2ss  23470  txtopon  23506  pttopon  23511  txcls  23519  ptclsg  23530  dfac14lem  23532  xkoccn  23534  txcnp  23535  ptcnplem  23536  txlm  23563  cnmpt2res  23592  cnmptkp  23595  cnmptk1  23596  cnmpt1k  23597  cnmptkk  23598  cnmptk1p  23600  cnmptk2  23601  xkoinjcn  23602  qtoptopon  23619  qtopcld  23628  qtoprest  23632  qtopcmap  23634  kqval  23641  regr1lem  23654  kqreglem1  23656  kqreglem2  23657  kqnrmlem1  23658  kqnrmlem2  23659  kqtop  23660  pt1hmeo  23721  xpstopnlem1  23724  xkohmeo  23730  neifil  23795  trnei  23807  elflim  23886  flimss1  23888  flimopn  23890  fbflim2  23892  flimcf  23897  flimclslem  23899  flffval  23904  flfnei  23906  flftg  23911  cnpflf2  23915  isfcls2  23928  fclsopn  23929  fclsnei  23934  fclscf  23940  fclscmp  23945  fcfval  23948  fcfnei  23950  cnpfcf  23956  tgpmulg2  24009  tmdgsum  24010  tmdgsum2  24011  subgntr  24022  opnsubg  24023  clssubg  24024  clsnsg  24025  cldsubg  24026  snclseqg  24031  tgphaus  24032  qustgpopn  24035  prdstgpd  24040  tsmsgsum  24054  tsmsid  24055  tgptsmscld  24066  mopntop  24355  metdseq0  24770  cnmpopc  24849  ishtpy  24898  om1val  24957  pi1val  24964  csscld  25176  clsocv  25177  relcmpcmet  25245  bcth2  25257  limcres  25814  perfdvf  25831  dvaddbr  25867  dvmulbr  25868  dvmulbrOLD  25869  dvcmulf  25875  dvmptres2  25893  dvmptcmul  25895  dvmptntr  25902  dvcnvlem  25907  lhop2  25947  lhop  25948  dvcnvrelem2  25950  taylthlem1  26308  zartop  33889  neibastop2  36405  neibastop3  36406  topjoin  36409  dissneqlem  37384  istopclsd  42803  dvresntr  46026