Theorem topontop 21764

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2112  ∪ cuni 4805  ‘cfv 6358  Topctop 21744  TopOnctopon 21761

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-iota 6316  df-fun 6360  df-fv 6366  df-topon 21762

This theorem is referenced by:  topontopi  21766  topontopon  21770  toprntopon  21776  toponmax  21777  topgele  21781  istps  21785  en2top  21836  pptbas  21859  toponmre  21944  cldmreon  21945  iscldtop  21946  neiptopreu  21984  resttopon  22012  resttopon2  22019  restlp  22034  restperf  22035  perfopn  22036  ordtopn3  22047  ordtcld1  22048  ordtcld2  22049  ordttop  22051  lmfval  22083  cnfval  22084  cnpfval  22085  tgcn  22103  tgcnp  22104  subbascn  22105  iscnp4  22114  iscncl  22120  cncls2  22124  cncls  22125  cnntr  22126  cncnp  22131  cnindis  22143  lmcls  22153  iscnrm2  22189  ist0-2  22195  ist1-2  22198  ishaus2  22202  hausnei2  22204  isreg2  22228  sscmp  22256  dfconn2  22270  clsconn  22281  conncompcld  22285  1stccnp  22313  locfincf  22382  kgenval  22386  kgenftop  22391  1stckgenlem  22404  kgen2ss  22406  txtopon  22442  pttopon  22447  txcls  22455  ptclsg  22466  dfac14lem  22468  xkoccn  22470  txcnp  22471  ptcnplem  22472  txlm  22499  cnmpt2res  22528  cnmptkp  22531  cnmptk1  22532  cnmpt1k  22533  cnmptkk  22534  cnmptk1p  22536  cnmptk2  22537  xkoinjcn  22538  qtoptopon  22555  qtopcld  22564  qtoprest  22568  qtopcmap  22570  kqval  22577  regr1lem  22590  kqreglem1  22592  kqreglem2  22593  kqnrmlem1  22594  kqnrmlem2  22595  kqtop  22596  pt1hmeo  22657  xpstopnlem1  22660  xkohmeo  22666  neifil  22731  trnei  22743  elflim  22822  flimss1  22824  flimopn  22826  fbflim2  22828  flimcf  22833  flimclslem  22835  flffval  22840  flfnei  22842  flftg  22847  cnpflf2  22851  isfcls2  22864  fclsopn  22865  fclsnei  22870  fclscf  22876  fclscmp  22881  fcfval  22884  fcfnei  22886  cnpfcf  22892  tgpmulg2  22945  tmdgsum  22946  tmdgsum2  22947  subgntr  22958  opnsubg  22959  clssubg  22960  clsnsg  22961  cldsubg  22962  snclseqg  22967  tgphaus  22968  qustgpopn  22971  prdstgpd  22976  tsmsgsum  22990  tsmsid  22991  tgptsmscld  23002  mopntop  23292  metdseq0  23705  cnmpopc  23779  ishtpy  23823  om1val  23881  pi1val  23888  csscld  24100  clsocv  24101  relcmpcmet  24169  bcth2  24181  limcres  24737  perfdvf  24754  dvaddbr  24789  dvmulbr  24790  dvcmulf  24796  dvmptres2  24813  dvmptcmul  24815  dvmptntr  24822  dvcnvlem  24827  lhop2  24866  lhop  24867  dvcnvrelem2  24869  taylthlem1  25219  zartop  31494  neibastop2  34236  neibastop3  34237  topjoin  34240  dissneqlem  35197  istopclsd  40166  dvresntr  43077