Theorem toponuni 22904

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  ∪ cuni 4845  ‘cfv 6492  Topctop 22883  TopOnctopon 22900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pow 5301  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-pw 4538  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6448  df-fun 6494  df-fv 6500  df-topon 22901

This theorem is referenced by:  toponunii  22906  toponmax  22916  toponss  22917  toponcom  22918  topgele  22920  topontopn  22930  toponmre  23083  cldmreon  23084  restuni  23152  resttopon2  23158  restlp  23173  restperf  23174  perfopn  23175  ordtcld1  23187  ordtcld2  23188  lmfval  23222  cnfval  23223  cnpfval  23224  cnpf2  23240  cnprcl2  23241  ssidcn  23245  iscnp4  23253  iscncl  23259  cncls2  23263  cncls  23264  cnntr  23265  cncnp  23270  lmcls  23292  lmcld  23293  iscnrm2  23328  ist0-2  23334  ist1-2  23337  ishaus2  23341  isreg2  23367  ordtt1  23369  sscmp  23395  dfconn2  23409  clsconn  23420  conncompcld  23424  1stccnp  23452  locfincf  23521  kgenval  23525  kgenuni  23529  1stckgenlem  23543  kgen2ss  23545  kgencn2  23547  txtopon  23581  txuni  23582  pttopon  23586  ptuniconst  23588  txcls  23594  ptclsg  23605  dfac14lem  23607  xkoccn  23609  ptcnplem  23611  ptcn  23617  cnmpt1t  23655  cnmpt2t  23663  cnmpt1res  23666  cnmpt2res  23667  cnmptkp  23670  cnmptk1p  23675  cnmptk2  23676  xkoinjcn  23677  elqtop3  23693  qtoptopon  23694  qtopcld  23703  qtoprest  23707  qtopcmap  23709  kqval  23716  kqcldsat  23723  isr0  23727  r0cld  23728  regr1lem  23729  kqnrmlem1  23733  kqnrmlem2  23734  pt1hmeo  23796  xpstopnlem1  23799  neifil  23870  trnei  23882  elflim  23961  flimss2  23962  flimss1  23963  flimopn  23965  fbflim2  23967  flimclslem  23974  flffval  23979  flfnei  23981  cnpflf2  23990  cnflf  23992  cnflf2  23993  isfcls2  24003  fclsopn  24004  fclsnei  24009  fclscmp  24020  ufilcmp  24022  fcfval  24023  fcfnei  24025  fcfelbas  24026  cnpfcf  24031  cnfcf  24032  alexsublem  24034  tmdcn2  24079  tmdgsum  24085  tmdgsum2  24086  symgtgp  24096  subgntr  24097  opnsubg  24098  clssubg  24099  clsnsg  24100  cldsubg  24101  tgpconncompeqg  24102  tgpconncomp  24103  ghmcnp  24105  snclseqg  24106  tgphaus  24107  tgpt1  24108  prdstmdd  24114  prdstgpd  24115  tsmsgsum  24129  tsmsid  24130  tsmsmhm  24136  tsmsadd  24137  tgptsmscld  24141  utop3cls  24241  mopnuni  24431  isxms2  24438  prdsxmslem2  24519  metdseq0  24845  cnmpopc  24920  ishtpy  24964  om1val  25022  pi1val  25029  csscld  25241  clsocv  25242  cfilfcls  25266  relcmpcmet  25310  limcres  25878  limccnp  25883  limccnp2  25884  dvbss  25893  perfdvf  25895  dvreslem  25901  dvres2lem  25902  dvcnp2  25912  dvaddbr  25930  dvmulbr  25931  dvcmulf  25937  dvmptres2  25954  dvmptcmul  25956  dvmptntr  25963  dvcnvrelem2  26010  ftc1cn  26035  taylthlem1  26363  ulmdvlem3  26392  efrlim  26958  zart0  34070  zarmxt1  34071  pl1cn  34146  cvxpconn  35477  cvxsconn  35478  ivthALT  36570  neibastop2  36596  neibastop3  36597  topmeet  36599  topjoin  36600  refsum2cnlem1  45492  dvresntr  46368  rrxunitopnfi  46742