Theorem toponuni 21811

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

Syntax hints:   → wi 4   = wceq 1543   ∈ wcel 2110  ∪ cuni 4819  ‘cfv 6380  Topctop 21790  TopOnctopon 21807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-iota 6338  df-fun 6382  df-fv 6388  df-topon 21808

This theorem is referenced by:  toponunii  21813  toponmax  21823  toponss  21824  toponcom  21825  topgele  21827  topontopn  21837  toponmre  21990  cldmreon  21991  restuni  22059  resttopon2  22065  restlp  22080  restperf  22081  perfopn  22082  ordtcld1  22094  ordtcld2  22095  lmfval  22129  cnfval  22130  cnpfval  22131  cnpf2  22147  cnprcl2  22148  ssidcn  22152  iscnp4  22160  iscncl  22166  cncls2  22170  cncls  22171  cnntr  22172  cncnp  22177  lmcls  22199  lmcld  22200  iscnrm2  22235  ist0-2  22241  ist1-2  22244  ishaus2  22248  isreg2  22274  ordtt1  22276  sscmp  22302  dfconn2  22316  clsconn  22327  conncompcld  22331  1stccnp  22359  locfincf  22428  kgenval  22432  kgenuni  22436  1stckgenlem  22450  kgen2ss  22452  kgencn2  22454  txtopon  22488  txuni  22489  pttopon  22493  ptuniconst  22495  txcls  22501  ptclsg  22512  dfac14lem  22514  xkoccn  22516  ptcnplem  22518  ptcn  22524  cnmpt1t  22562  cnmpt2t  22570  cnmpt1res  22573  cnmpt2res  22574  cnmptkp  22577  cnmptk1p  22582  cnmptk2  22583  xkoinjcn  22584  elqtop3  22600  qtoptopon  22601  qtopcld  22610  qtoprest  22614  qtopcmap  22616  kqval  22623  kqcldsat  22630  isr0  22634  r0cld  22635  regr1lem  22636  kqnrmlem1  22640  kqnrmlem2  22641  pt1hmeo  22703  xpstopnlem1  22706  neifil  22777  trnei  22789  elflim  22868  flimss2  22869  flimss1  22870  flimopn  22872  fbflim2  22874  flimclslem  22881  flffval  22886  flfnei  22888  cnpflf2  22897  cnflf  22899  cnflf2  22900  isfcls2  22910  fclsopn  22911  fclsnei  22916  fclscmp  22927  ufilcmp  22929  fcfval  22930  fcfnei  22932  fcfelbas  22933  cnpfcf  22938  cnfcf  22939  alexsublem  22941  tmdcn2  22986  tmdgsum  22992  tmdgsum2  22993  symgtgp  23003  subgntr  23004  opnsubg  23005  clssubg  23006  clsnsg  23007  cldsubg  23008  tgpconncompeqg  23009  tgpconncomp  23010  ghmcnp  23012  snclseqg  23013  tgphaus  23014  tgpt1  23015  prdstmdd  23021  prdstgpd  23022  tsmsgsum  23036  tsmsid  23037  tsmsmhm  23043  tsmsadd  23044  tgptsmscld  23048  utop3cls  23149  mopnuni  23339  isxms2  23346  prdsxmslem2  23427  metdseq0  23751  cnmpopc  23825  ishtpy  23869  om1val  23927  pi1val  23934  csscld  24146  clsocv  24147  cfilfcls  24171  relcmpcmet  24215  limcres  24783  limccnp  24788  limccnp2  24789  dvbss  24798  perfdvf  24800  dvreslem  24806  dvres2lem  24807  dvcnp2  24817  dvaddbr  24835  dvmulbr  24836  dvcmulf  24842  dvmptres2  24859  dvmptcmul  24861  dvmptntr  24868  dvcnvrelem2  24915  ftc1cn  24940  taylthlem1  25265  ulmdvlem3  25294  efrlim  25852  zart0  31543  zarmxt1  31544  pl1cn  31619  cvxpconn  32917  cvxsconn  32918  ivthALT  34261  neibastop2  34287  neibastop3  34288  topmeet  34290  topjoin  34291  refsum2cnlem1  42253  dvresntr  43134  rrxunitopnfi  43508