Theorem toponuni 22858

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ cuni 4863  ‘cfv 6492  Topctop 22837  TopOnctopon 22854

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fv 6500  df-topon 22855

This theorem is referenced by:  toponunii  22860  toponmax  22870  toponss  22871  toponcom  22872  topgele  22874  topontopn  22884  toponmre  23037  cldmreon  23038  restuni  23106  resttopon2  23112  restlp  23127  restperf  23128  perfopn  23129  ordtcld1  23141  ordtcld2  23142  lmfval  23176  cnfval  23177  cnpfval  23178  cnpf2  23194  cnprcl2  23195  ssidcn  23199  iscnp4  23207  iscncl  23213  cncls2  23217  cncls  23218  cnntr  23219  cncnp  23224  lmcls  23246  lmcld  23247  iscnrm2  23282  ist0-2  23288  ist1-2  23291  ishaus2  23295  isreg2  23321  ordtt1  23323  sscmp  23349  dfconn2  23363  clsconn  23374  conncompcld  23378  1stccnp  23406  locfincf  23475  kgenval  23479  kgenuni  23483  1stckgenlem  23497  kgen2ss  23499  kgencn2  23501  txtopon  23535  txuni  23536  pttopon  23540  ptuniconst  23542  txcls  23548  ptclsg  23559  dfac14lem  23561  xkoccn  23563  ptcnplem  23565  ptcn  23571  cnmpt1t  23609  cnmpt2t  23617  cnmpt1res  23620  cnmpt2res  23621  cnmptkp  23624  cnmptk1p  23629  cnmptk2  23630  xkoinjcn  23631  elqtop3  23647  qtoptopon  23648  qtopcld  23657  qtoprest  23661  qtopcmap  23663  kqval  23670  kqcldsat  23677  isr0  23681  r0cld  23682  regr1lem  23683  kqnrmlem1  23687  kqnrmlem2  23688  pt1hmeo  23750  xpstopnlem1  23753  neifil  23824  trnei  23836  elflim  23915  flimss2  23916  flimss1  23917  flimopn  23919  fbflim2  23921  flimclslem  23928  flffval  23933  flfnei  23935  cnpflf2  23944  cnflf  23946  cnflf2  23947  isfcls2  23957  fclsopn  23958  fclsnei  23963  fclscmp  23974  ufilcmp  23976  fcfval  23977  fcfnei  23979  fcfelbas  23980  cnpfcf  23985  cnfcf  23986  alexsublem  23988  tmdcn2  24033  tmdgsum  24039  tmdgsum2  24040  symgtgp  24050  subgntr  24051  opnsubg  24052  clssubg  24053  clsnsg  24054  cldsubg  24055  tgpconncompeqg  24056  tgpconncomp  24057  ghmcnp  24059  snclseqg  24060  tgphaus  24061  tgpt1  24062  prdstmdd  24068  prdstgpd  24069  tsmsgsum  24083  tsmsid  24084  tsmsmhm  24090  tsmsadd  24091  tgptsmscld  24095  utop3cls  24195  mopnuni  24385  isxms2  24392  prdsxmslem2  24473  metdseq0  24799  cnmpopc  24878  ishtpy  24927  om1val  24986  pi1val  24993  csscld  25205  clsocv  25206  cfilfcls  25230  relcmpcmet  25274  limcres  25843  limccnp  25848  limccnp2  25849  dvbss  25858  perfdvf  25860  dvreslem  25866  dvres2lem  25867  dvcnp2  25877  dvcnp2OLD  25878  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcmulf  25904  dvmptres2  25922  dvmptcmul  25924  dvmptntr  25931  dvcnvrelem2  25979  ftc1cn  26006  taylthlem1  26337  ulmdvlem3  26367  efrlim  26935  efrlimOLD  26936  zart0  34036  zarmxt1  34037  pl1cn  34112  cvxpconn  35436  cvxsconn  35437  ivthALT  36529  neibastop2  36555  neibastop3  36556  topmeet  36558  topjoin  36559  refsum2cnlem1  45282  dvresntr  46162  rrxunitopnfi  46536