Theorem toponuni 22852

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ cuni 4883  ‘cfv 6531  Topctop 22831  TopOnctopon 22848

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6484  df-fun 6533  df-fv 6539  df-topon 22849

This theorem is referenced by:  toponunii  22854  toponmax  22864  toponss  22865  toponcom  22866  topgele  22868  topontopn  22878  toponmre  23031  cldmreon  23032  restuni  23100  resttopon2  23106  restlp  23121  restperf  23122  perfopn  23123  ordtcld1  23135  ordtcld2  23136  lmfval  23170  cnfval  23171  cnpfval  23172  cnpf2  23188  cnprcl2  23189  ssidcn  23193  iscnp4  23201  iscncl  23207  cncls2  23211  cncls  23212  cnntr  23213  cncnp  23218  lmcls  23240  lmcld  23241  iscnrm2  23276  ist0-2  23282  ist1-2  23285  ishaus2  23289  isreg2  23315  ordtt1  23317  sscmp  23343  dfconn2  23357  clsconn  23368  conncompcld  23372  1stccnp  23400  locfincf  23469  kgenval  23473  kgenuni  23477  1stckgenlem  23491  kgen2ss  23493  kgencn2  23495  txtopon  23529  txuni  23530  pttopon  23534  ptuniconst  23536  txcls  23542  ptclsg  23553  dfac14lem  23555  xkoccn  23557  ptcnplem  23559  ptcn  23565  cnmpt1t  23603  cnmpt2t  23611  cnmpt1res  23614  cnmpt2res  23615  cnmptkp  23618  cnmptk1p  23623  cnmptk2  23624  xkoinjcn  23625  elqtop3  23641  qtoptopon  23642  qtopcld  23651  qtoprest  23655  qtopcmap  23657  kqval  23664  kqcldsat  23671  isr0  23675  r0cld  23676  regr1lem  23677  kqnrmlem1  23681  kqnrmlem2  23682  pt1hmeo  23744  xpstopnlem1  23747  neifil  23818  trnei  23830  elflim  23909  flimss2  23910  flimss1  23911  flimopn  23913  fbflim2  23915  flimclslem  23922  flffval  23927  flfnei  23929  cnpflf2  23938  cnflf  23940  cnflf2  23941  isfcls2  23951  fclsopn  23952  fclsnei  23957  fclscmp  23968  ufilcmp  23970  fcfval  23971  fcfnei  23973  fcfelbas  23974  cnpfcf  23979  cnfcf  23980  alexsublem  23982  tmdcn2  24027  tmdgsum  24033  tmdgsum2  24034  symgtgp  24044  subgntr  24045  opnsubg  24046  clssubg  24047  clsnsg  24048  cldsubg  24049  tgpconncompeqg  24050  tgpconncomp  24051  ghmcnp  24053  snclseqg  24054  tgphaus  24055  tgpt1  24056  prdstmdd  24062  prdstgpd  24063  tsmsgsum  24077  tsmsid  24078  tsmsmhm  24084  tsmsadd  24085  tgptsmscld  24089  utop3cls  24190  mopnuni  24380  isxms2  24387  prdsxmslem2  24468  metdseq0  24794  cnmpopc  24873  ishtpy  24922  om1val  24981  pi1val  24988  csscld  25201  clsocv  25202  cfilfcls  25226  relcmpcmet  25270  limcres  25839  limccnp  25844  limccnp2  25845  dvbss  25854  perfdvf  25856  dvreslem  25862  dvres2lem  25863  dvcnp2  25873  dvcnp2OLD  25874  dvaddbr  25892  dvmulbr  25893  dvmulbrOLD  25894  dvcmulf  25900  dvmptres2  25918  dvmptcmul  25920  dvmptntr  25927  dvcnvrelem2  25975  ftc1cn  26002  taylthlem1  26333  ulmdvlem3  26363  efrlim  26931  efrlimOLD  26932  zart0  33910  zarmxt1  33911  pl1cn  33986  cvxpconn  35264  cvxsconn  35265  ivthALT  36353  neibastop2  36379  neibastop3  36380  topmeet  36382  topjoin  36383  refsum2cnlem1  45061  dvresntr  45947  rrxunitopnfi  46321