Theorem toponuni 22736

Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.)

Assertion

Ref	Expression
toponuni	⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)

Proof of Theorem toponuni

Step	Hyp	Ref	Expression
1		istopon 22734	. 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽))
2	1	simprbi 496	1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2105  ∪ cuni 4908  ‘cfv 6543  Topctop 22715  TopOnctopon 22732

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-topon 22733

This theorem is referenced by:  toponunii  22738  toponmax  22748  toponss  22749  toponcom  22750  topgele  22752  topontopn  22762  toponmre  22917  cldmreon  22918  restuni  22986  resttopon2  22992  restlp  23007  restperf  23008  perfopn  23009  ordtcld1  23021  ordtcld2  23022  lmfval  23056  cnfval  23057  cnpfval  23058  cnpf2  23074  cnprcl2  23075  ssidcn  23079  iscnp4  23087  iscncl  23093  cncls2  23097  cncls  23098  cnntr  23099  cncnp  23104  lmcls  23126  lmcld  23127  iscnrm2  23162  ist0-2  23168  ist1-2  23171  ishaus2  23175  isreg2  23201  ordtt1  23203  sscmp  23229  dfconn2  23243  clsconn  23254  conncompcld  23258  1stccnp  23286  locfincf  23355  kgenval  23359  kgenuni  23363  1stckgenlem  23377  kgen2ss  23379  kgencn2  23381  txtopon  23415  txuni  23416  pttopon  23420  ptuniconst  23422  txcls  23428  ptclsg  23439  dfac14lem  23441  xkoccn  23443  ptcnplem  23445  ptcn  23451  cnmpt1t  23489  cnmpt2t  23497  cnmpt1res  23500  cnmpt2res  23501  cnmptkp  23504  cnmptk1p  23509  cnmptk2  23510  xkoinjcn  23511  elqtop3  23527  qtoptopon  23528  qtopcld  23537  qtoprest  23541  qtopcmap  23543  kqval  23550  kqcldsat  23557  isr0  23561  r0cld  23562  regr1lem  23563  kqnrmlem1  23567  kqnrmlem2  23568  pt1hmeo  23630  xpstopnlem1  23633  neifil  23704  trnei  23716  elflim  23795  flimss2  23796  flimss1  23797  flimopn  23799  fbflim2  23801  flimclslem  23808  flffval  23813  flfnei  23815  cnpflf2  23824  cnflf  23826  cnflf2  23827  isfcls2  23837  fclsopn  23838  fclsnei  23843  fclscmp  23854  ufilcmp  23856  fcfval  23857  fcfnei  23859  fcfelbas  23860  cnpfcf  23865  cnfcf  23866  alexsublem  23868  tmdcn2  23913  tmdgsum  23919  tmdgsum2  23920  symgtgp  23930  subgntr  23931  opnsubg  23932  clssubg  23933  clsnsg  23934  cldsubg  23935  tgpconncompeqg  23936  tgpconncomp  23937  ghmcnp  23939  snclseqg  23940  tgphaus  23941  tgpt1  23942  prdstmdd  23948  prdstgpd  23949  tsmsgsum  23963  tsmsid  23964  tsmsmhm  23970  tsmsadd  23971  tgptsmscld  23975  utop3cls  24076  mopnuni  24267  isxms2  24274  prdsxmslem2  24358  metdseq0  24690  cnmpopc  24769  ishtpy  24818  om1val  24877  pi1val  24884  csscld  25097  clsocv  25098  cfilfcls  25122  relcmpcmet  25166  limcres  25735  limccnp  25740  limccnp2  25741  dvbss  25750  perfdvf  25752  dvreslem  25758  dvres2lem  25759  dvcnp2  25769  dvcnp2OLD  25770  dvaddbr  25788  dvmulbr  25789  dvmulbrOLD  25790  dvcmulf  25796  dvmptres2  25814  dvmptcmul  25816  dvmptntr  25823  dvcnvrelem2  25871  ftc1cn  25898  taylthlem1  26224  ulmdvlem3  26253  efrlim  26815  zart0  33323  zarmxt1  33324  pl1cn  33399  cvxpconn  34697  cvxsconn  34698  ivthALT  35684  neibastop2  35710  neibastop3  35711  topmeet  35713  topjoin  35714  refsum2cnlem1  44184  dvresntr  45093  rrxunitopnfi  45467