Theorem toponuni 22817

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4861  ‘cfv 6486  Topctop 22796  TopOnctopon 22813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fv 6494  df-topon 22814

This theorem is referenced by:  toponunii  22819  toponmax  22829  toponss  22830  toponcom  22831  topgele  22833  topontopn  22843  toponmre  22996  cldmreon  22997  restuni  23065  resttopon2  23071  restlp  23086  restperf  23087  perfopn  23088  ordtcld1  23100  ordtcld2  23101  lmfval  23135  cnfval  23136  cnpfval  23137  cnpf2  23153  cnprcl2  23154  ssidcn  23158  iscnp4  23166  iscncl  23172  cncls2  23176  cncls  23177  cnntr  23178  cncnp  23183  lmcls  23205  lmcld  23206  iscnrm2  23241  ist0-2  23247  ist1-2  23250  ishaus2  23254  isreg2  23280  ordtt1  23282  sscmp  23308  dfconn2  23322  clsconn  23333  conncompcld  23337  1stccnp  23365  locfincf  23434  kgenval  23438  kgenuni  23442  1stckgenlem  23456  kgen2ss  23458  kgencn2  23460  txtopon  23494  txuni  23495  pttopon  23499  ptuniconst  23501  txcls  23507  ptclsg  23518  dfac14lem  23520  xkoccn  23522  ptcnplem  23524  ptcn  23530  cnmpt1t  23568  cnmpt2t  23576  cnmpt1res  23579  cnmpt2res  23580  cnmptkp  23583  cnmptk1p  23588  cnmptk2  23589  xkoinjcn  23590  elqtop3  23606  qtoptopon  23607  qtopcld  23616  qtoprest  23620  qtopcmap  23622  kqval  23629  kqcldsat  23636  isr0  23640  r0cld  23641  regr1lem  23642  kqnrmlem1  23646  kqnrmlem2  23647  pt1hmeo  23709  xpstopnlem1  23712  neifil  23783  trnei  23795  elflim  23874  flimss2  23875  flimss1  23876  flimopn  23878  fbflim2  23880  flimclslem  23887  flffval  23892  flfnei  23894  cnpflf2  23903  cnflf  23905  cnflf2  23906  isfcls2  23916  fclsopn  23917  fclsnei  23922  fclscmp  23933  ufilcmp  23935  fcfval  23936  fcfnei  23938  fcfelbas  23939  cnpfcf  23944  cnfcf  23945  alexsublem  23947  tmdcn2  23992  tmdgsum  23998  tmdgsum2  23999  symgtgp  24009  subgntr  24010  opnsubg  24011  clssubg  24012  clsnsg  24013  cldsubg  24014  tgpconncompeqg  24015  tgpconncomp  24016  ghmcnp  24018  snclseqg  24019  tgphaus  24020  tgpt1  24021  prdstmdd  24027  prdstgpd  24028  tsmsgsum  24042  tsmsid  24043  tsmsmhm  24049  tsmsadd  24050  tgptsmscld  24054  utop3cls  24155  mopnuni  24345  isxms2  24352  prdsxmslem2  24433  metdseq0  24759  cnmpopc  24838  ishtpy  24887  om1val  24946  pi1val  24953  csscld  25165  clsocv  25166  cfilfcls  25190  relcmpcmet  25234  limcres  25803  limccnp  25808  limccnp2  25809  dvbss  25818  perfdvf  25820  dvreslem  25826  dvres2lem  25827  dvcnp2  25837  dvcnp2OLD  25838  dvaddbr  25856  dvmulbr  25857  dvmulbrOLD  25858  dvcmulf  25864  dvmptres2  25882  dvmptcmul  25884  dvmptntr  25891  dvcnvrelem2  25939  ftc1cn  25966  taylthlem1  26297  ulmdvlem3  26327  efrlim  26895  efrlimOLD  26896  zart0  33848  zarmxt1  33849  pl1cn  33924  cvxpconn  35217  cvxsconn  35218  ivthALT  36311  neibastop2  36337  neibastop3  36338  topmeet  36340  topjoin  36341  refsum2cnlem1  45018  dvresntr  45903  rrxunitopnfi  46277