Theorem toponuni 23052

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  ∪ cuni 4873  ‘cfv 6538  Topctop 23031  TopOnctopon 23048

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6494  df-fun 6540  df-fv 6546  df-topon 23049

This theorem is referenced by:  toponunii  23054  toponmax  23064  toponss  23065  toponcom  23066  topgele  23068  topontopn  23078  toponmre  23231  cldmreon  23232  restuni  23300  resttopon2  23306  restlp  23321  restperf  23322  perfopn  23323  ordtcld1  23335  ordtcld2  23336  lmfval  23370  cnfval  23371  cnpfval  23372  cnpf2  23388  cnprcl2  23389  ssidcn  23393  iscnp4  23401  iscncl  23407  cncls2  23411  cncls  23412  cnntr  23413  cncnp  23418  lmcls  23440  lmcld  23441  iscnrm2  23476  ist0-2  23482  ist1-2  23485  ishaus2  23489  isreg2  23515  ordtt1  23517  sscmp  23543  dfconn2  23557  clsconn  23568  conncompcld  23572  1stccnp  23600  locfincf  23669  kgenval  23673  kgenuni  23677  1stckgenlem  23691  kgen2ss  23693  kgencn2  23695  txtopon  23729  txuni  23730  pttopon  23734  ptuniconst  23736  txcls  23742  ptclsg  23753  dfac14lem  23755  xkoccn  23757  ptcnplem  23759  ptcn  23765  cnmpt1t  23803  cnmpt2t  23811  cnmpt1res  23814  cnmpt2res  23815  cnmptkp  23818  cnmptk1p  23823  cnmptk2  23824  xkoinjcn  23825  elqtop3  23841  qtoptopon  23842  qtopcld  23851  qtoprest  23855  qtopcmap  23857  kqval  23864  kqcldsat  23871  isr0  23875  r0cld  23876  regr1lem  23877  kqnrmlem1  23881  kqnrmlem2  23882  pt1hmeo  23944  xpstopnlem1  23947  neifil  24018  trnei  24030  elflim  24109  flimss2  24110  flimss1  24111  flimopn  24113  fbflim2  24115  flimclslem  24122  flffval  24127  flfnei  24129  cnpflf2  24138  cnflf  24140  cnflf2  24141  isfcls2  24151  fclsopn  24152  fclsnei  24157  fclscmp  24168  ufilcmp  24170  fcfval  24171  fcfnei  24173  fcfelbas  24174  cnpfcf  24179  cnfcf  24180  alexsublem  24182  tmdcn2  24227  tmdgsum  24233  tmdgsum2  24234  symgtgp  24244  subgntr  24245  opnsubg  24246  clssubg  24247  clsnsg  24248  cldsubg  24249  tgpconncompeqg  24250  tgpconncomp  24251  ghmcnp  24253  snclseqg  24254  tgphaus  24255  tgpt1  24256  prdstmdd  24262  prdstgpd  24263  tsmsgsum  24277  tsmsid  24278  tsmsmhm  24284  tsmsadd  24285  tgptsmscld  24289  utop3cls  24389  mopnuni  24579  isxms2  24586  prdsxmslem2  24667  metdseq0  24993  cnmpopc  25068  ishtpy  25112  om1val  25170  pi1val  25177  csscld  25389  clsocv  25390  cfilfcls  25414  relcmpcmet  25458  limcres  26026  limccnp  26031  limccnp2  26032  dvbss  26041  perfdvf  26043  dvreslem  26049  dvres2lem  26050  dvcnp2  26060  dvaddbr  26078  dvmulbr  26079  dvcmulf  26085  dvmptres2  26102  dvmptcmul  26104  dvmptntr  26111  dvcnvrelem2  26158  ftc1cn  26183  taylthlem1  26517  ulmdvlem3  26546  efrlim  27115  zart0  34250  zarmxt1  34251  pl1cn  34326  cvxpconn  35715  cvxsconn  35716  ivthALT  36827  neibastop2  36853  neibastop3  36854  topmeet  36856  topjoin  36857  refsum2cnlem1  45740  dvresntr  46615  rrxunitopnfi  46989