Theorem toponuni 22920

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ∪ cuni 4907  ‘cfv 6561  Topctop 22899  TopOnctopon 22916

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 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fv 6569  df-topon 22917

This theorem is referenced by:  toponunii  22922  toponmax  22932  toponss  22933  toponcom  22934  topgele  22936  topontopn  22946  toponmre  23101  cldmreon  23102  restuni  23170  resttopon2  23176  restlp  23191  restperf  23192  perfopn  23193  ordtcld1  23205  ordtcld2  23206  lmfval  23240  cnfval  23241  cnpfval  23242  cnpf2  23258  cnprcl2  23259  ssidcn  23263  iscnp4  23271  iscncl  23277  cncls2  23281  cncls  23282  cnntr  23283  cncnp  23288  lmcls  23310  lmcld  23311  iscnrm2  23346  ist0-2  23352  ist1-2  23355  ishaus2  23359  isreg2  23385  ordtt1  23387  sscmp  23413  dfconn2  23427  clsconn  23438  conncompcld  23442  1stccnp  23470  locfincf  23539  kgenval  23543  kgenuni  23547  1stckgenlem  23561  kgen2ss  23563  kgencn2  23565  txtopon  23599  txuni  23600  pttopon  23604  ptuniconst  23606  txcls  23612  ptclsg  23623  dfac14lem  23625  xkoccn  23627  ptcnplem  23629  ptcn  23635  cnmpt1t  23673  cnmpt2t  23681  cnmpt1res  23684  cnmpt2res  23685  cnmptkp  23688  cnmptk1p  23693  cnmptk2  23694  xkoinjcn  23695  elqtop3  23711  qtoptopon  23712  qtopcld  23721  qtoprest  23725  qtopcmap  23727  kqval  23734  kqcldsat  23741  isr0  23745  r0cld  23746  regr1lem  23747  kqnrmlem1  23751  kqnrmlem2  23752  pt1hmeo  23814  xpstopnlem1  23817  neifil  23888  trnei  23900  elflim  23979  flimss2  23980  flimss1  23981  flimopn  23983  fbflim2  23985  flimclslem  23992  flffval  23997  flfnei  23999  cnpflf2  24008  cnflf  24010  cnflf2  24011  isfcls2  24021  fclsopn  24022  fclsnei  24027  fclscmp  24038  ufilcmp  24040  fcfval  24041  fcfnei  24043  fcfelbas  24044  cnpfcf  24049  cnfcf  24050  alexsublem  24052  tmdcn2  24097  tmdgsum  24103  tmdgsum2  24104  symgtgp  24114  subgntr  24115  opnsubg  24116  clssubg  24117  clsnsg  24118  cldsubg  24119  tgpconncompeqg  24120  tgpconncomp  24121  ghmcnp  24123  snclseqg  24124  tgphaus  24125  tgpt1  24126  prdstmdd  24132  prdstgpd  24133  tsmsgsum  24147  tsmsid  24148  tsmsmhm  24154  tsmsadd  24155  tgptsmscld  24159  utop3cls  24260  mopnuni  24451  isxms2  24458  prdsxmslem2  24542  metdseq0  24876  cnmpopc  24955  ishtpy  25004  om1val  25063  pi1val  25070  csscld  25283  clsocv  25284  cfilfcls  25308  relcmpcmet  25352  limcres  25921  limccnp  25926  limccnp2  25927  dvbss  25936  perfdvf  25938  dvreslem  25944  dvres2lem  25945  dvcnp2  25955  dvcnp2OLD  25956  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmulf  25982  dvmptres2  26000  dvmptcmul  26002  dvmptntr  26009  dvcnvrelem2  26057  ftc1cn  26084  taylthlem1  26415  ulmdvlem3  26445  efrlim  27012  efrlimOLD  27013  zart0  33878  zarmxt1  33879  pl1cn  33954  cvxpconn  35247  cvxsconn  35248  ivthALT  36336  neibastop2  36362  neibastop3  36363  topmeet  36365  topjoin  36366  refsum2cnlem1  45042  dvresntr  45933  rrxunitopnfi  46307