Theorem toponuni 22808

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4874  ‘cfv 6514  Topctop 22787  TopOnctopon 22804

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-iota 6467  df-fun 6516  df-fv 6522  df-topon 22805

This theorem is referenced by:  toponunii  22810  toponmax  22820  toponss  22821  toponcom  22822  topgele  22824  topontopn  22834  toponmre  22987  cldmreon  22988  restuni  23056  resttopon2  23062  restlp  23077  restperf  23078  perfopn  23079  ordtcld1  23091  ordtcld2  23092  lmfval  23126  cnfval  23127  cnpfval  23128  cnpf2  23144  cnprcl2  23145  ssidcn  23149  iscnp4  23157  iscncl  23163  cncls2  23167  cncls  23168  cnntr  23169  cncnp  23174  lmcls  23196  lmcld  23197  iscnrm2  23232  ist0-2  23238  ist1-2  23241  ishaus2  23245  isreg2  23271  ordtt1  23273  sscmp  23299  dfconn2  23313  clsconn  23324  conncompcld  23328  1stccnp  23356  locfincf  23425  kgenval  23429  kgenuni  23433  1stckgenlem  23447  kgen2ss  23449  kgencn2  23451  txtopon  23485  txuni  23486  pttopon  23490  ptuniconst  23492  txcls  23498  ptclsg  23509  dfac14lem  23511  xkoccn  23513  ptcnplem  23515  ptcn  23521  cnmpt1t  23559  cnmpt2t  23567  cnmpt1res  23570  cnmpt2res  23571  cnmptkp  23574  cnmptk1p  23579  cnmptk2  23580  xkoinjcn  23581  elqtop3  23597  qtoptopon  23598  qtopcld  23607  qtoprest  23611  qtopcmap  23613  kqval  23620  kqcldsat  23627  isr0  23631  r0cld  23632  regr1lem  23633  kqnrmlem1  23637  kqnrmlem2  23638  pt1hmeo  23700  xpstopnlem1  23703  neifil  23774  trnei  23786  elflim  23865  flimss2  23866  flimss1  23867  flimopn  23869  fbflim2  23871  flimclslem  23878  flffval  23883  flfnei  23885  cnpflf2  23894  cnflf  23896  cnflf2  23897  isfcls2  23907  fclsopn  23908  fclsnei  23913  fclscmp  23924  ufilcmp  23926  fcfval  23927  fcfnei  23929  fcfelbas  23930  cnpfcf  23935  cnfcf  23936  alexsublem  23938  tmdcn2  23983  tmdgsum  23989  tmdgsum2  23990  symgtgp  24000  subgntr  24001  opnsubg  24002  clssubg  24003  clsnsg  24004  cldsubg  24005  tgpconncompeqg  24006  tgpconncomp  24007  ghmcnp  24009  snclseqg  24010  tgphaus  24011  tgpt1  24012  prdstmdd  24018  prdstgpd  24019  tsmsgsum  24033  tsmsid  24034  tsmsmhm  24040  tsmsadd  24041  tgptsmscld  24045  utop3cls  24146  mopnuni  24336  isxms2  24343  prdsxmslem2  24424  metdseq0  24750  cnmpopc  24829  ishtpy  24878  om1val  24937  pi1val  24944  csscld  25156  clsocv  25157  cfilfcls  25181  relcmpcmet  25225  limcres  25794  limccnp  25799  limccnp2  25800  dvbss  25809  perfdvf  25811  dvreslem  25817  dvres2lem  25818  dvcnp2  25828  dvcnp2OLD  25829  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmulf  25855  dvmptres2  25873  dvmptcmul  25875  dvmptntr  25882  dvcnvrelem2  25930  ftc1cn  25957  taylthlem1  26288  ulmdvlem3  26318  efrlim  26886  efrlimOLD  26887  zart0  33876  zarmxt1  33877  pl1cn  33952  cvxpconn  35236  cvxsconn  35237  ivthALT  36330  neibastop2  36356  neibastop3  36357  topmeet  36359  topjoin  36360  refsum2cnlem1  45038  dvresntr  45923  rrxunitopnfi  46297