Theorem toponuni 22889

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ cuni 4851  ‘cfv 6492  Topctop 22868  TopOnctopon 22885

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  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 22886

This theorem is referenced by:  toponunii  22891  toponmax  22901  toponss  22902  toponcom  22903  topgele  22905  topontopn  22915  toponmre  23068  cldmreon  23069  restuni  23137  resttopon2  23143  restlp  23158  restperf  23159  perfopn  23160  ordtcld1  23172  ordtcld2  23173  lmfval  23207  cnfval  23208  cnpfval  23209  cnpf2  23225  cnprcl2  23226  ssidcn  23230  iscnp4  23238  iscncl  23244  cncls2  23248  cncls  23249  cnntr  23250  cncnp  23255  lmcls  23277  lmcld  23278  iscnrm2  23313  ist0-2  23319  ist1-2  23322  ishaus2  23326  isreg2  23352  ordtt1  23354  sscmp  23380  dfconn2  23394  clsconn  23405  conncompcld  23409  1stccnp  23437  locfincf  23506  kgenval  23510  kgenuni  23514  1stckgenlem  23528  kgen2ss  23530  kgencn2  23532  txtopon  23566  txuni  23567  pttopon  23571  ptuniconst  23573  txcls  23579  ptclsg  23590  dfac14lem  23592  xkoccn  23594  ptcnplem  23596  ptcn  23602  cnmpt1t  23640  cnmpt2t  23648  cnmpt1res  23651  cnmpt2res  23652  cnmptkp  23655  cnmptk1p  23660  cnmptk2  23661  xkoinjcn  23662  elqtop3  23678  qtoptopon  23679  qtopcld  23688  qtoprest  23692  qtopcmap  23694  kqval  23701  kqcldsat  23708  isr0  23712  r0cld  23713  regr1lem  23714  kqnrmlem1  23718  kqnrmlem2  23719  pt1hmeo  23781  xpstopnlem1  23784  neifil  23855  trnei  23867  elflim  23946  flimss2  23947  flimss1  23948  flimopn  23950  fbflim2  23952  flimclslem  23959  flffval  23964  flfnei  23966  cnpflf2  23975  cnflf  23977  cnflf2  23978  isfcls2  23988  fclsopn  23989  fclsnei  23994  fclscmp  24005  ufilcmp  24007  fcfval  24008  fcfnei  24010  fcfelbas  24011  cnpfcf  24016  cnfcf  24017  alexsublem  24019  tmdcn2  24064  tmdgsum  24070  tmdgsum2  24071  symgtgp  24081  subgntr  24082  opnsubg  24083  clssubg  24084  clsnsg  24085  cldsubg  24086  tgpconncompeqg  24087  tgpconncomp  24088  ghmcnp  24090  snclseqg  24091  tgphaus  24092  tgpt1  24093  prdstmdd  24099  prdstgpd  24100  tsmsgsum  24114  tsmsid  24115  tsmsmhm  24121  tsmsadd  24122  tgptsmscld  24126  utop3cls  24226  mopnuni  24416  isxms2  24423  prdsxmslem2  24504  metdseq0  24830  cnmpopc  24905  ishtpy  24949  om1val  25007  pi1val  25014  csscld  25226  clsocv  25227  cfilfcls  25251  relcmpcmet  25295  limcres  25863  limccnp  25868  limccnp2  25869  dvbss  25878  perfdvf  25880  dvreslem  25886  dvres2lem  25887  dvcnp2  25897  dvaddbr  25915  dvmulbr  25916  dvcmulf  25922  dvmptres2  25939  dvmptcmul  25941  dvmptntr  25948  dvcnvrelem2  25995  ftc1cn  26020  taylthlem1  26350  ulmdvlem3  26380  efrlim  26946  efrlimOLD  26947  zart0  34039  zarmxt1  34040  pl1cn  34115  cvxpconn  35440  cvxsconn  35441  ivthALT  36533  neibastop2  36559  neibastop3  36560  topmeet  36562  topjoin  36563  refsum2cnlem1  45486  dvresntr  46364  rrxunitopnfi  46738