Theorem toponuni 21242

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

Syntax hints:   → wi 4   = wceq 1508   ∈ wcel 2051  ∪ cuni 4709  ‘cfv 6186  Topctop 21221  TopOnctopon 21238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-iota 6150  df-fun 6188  df-fv 6194  df-topon 21239

This theorem is referenced by:  toponunii  21244  toponmax  21254  toponss  21255  toponcom  21256  topgele  21258  topontopn  21268  toponmre  21421  cldmreon  21422  restuni  21490  resttopon2  21496  restlp  21511  restperf  21512  perfopn  21513  ordtcld1  21525  ordtcld2  21526  lmfval  21560  cnfval  21561  cnpfval  21562  cnpf2  21578  cnprcl2  21579  ssidcn  21583  iscnp4  21591  iscncl  21597  cncls2  21601  cncls  21602  cnntr  21603  cncnp  21608  lmcls  21630  lmcld  21631  iscnrm2  21666  ist0-2  21672  ist1-2  21675  ishaus2  21679  isreg2  21705  ordtt1  21707  sscmp  21733  dfconn2  21747  clsconn  21758  conncompcld  21762  1stccnp  21790  locfincf  21859  kgenval  21863  kgenuni  21867  1stckgenlem  21881  kgen2ss  21883  kgencn2  21885  txtopon  21919  txuni  21920  pttopon  21924  ptuniconst  21926  txcls  21932  ptclsg  21943  dfac14lem  21945  xkoccn  21947  ptcnplem  21949  ptcn  21955  cnmpt1t  21993  cnmpt2t  22001  cnmpt1res  22004  cnmpt2res  22005  cnmptkp  22008  cnmptk1p  22013  cnmptk2  22014  xkoinjcn  22015  elqtop3  22031  qtoptopon  22032  qtopcld  22041  qtoprest  22045  qtopcmap  22047  kqval  22054  kqcldsat  22061  isr0  22065  r0cld  22066  regr1lem  22067  kqnrmlem1  22071  kqnrmlem2  22072  pt1hmeo  22134  xpstopnlem1  22137  neifil  22208  trnei  22220  elflim  22299  flimss2  22300  flimss1  22301  flimopn  22303  fbflim2  22305  flimclslem  22312  flffval  22317  flfnei  22319  cnpflf2  22328  cnflf  22330  cnflf2  22331  isfcls2  22341  fclsopn  22342  fclsnei  22347  fclscmp  22358  ufilcmp  22360  fcfval  22361  fcfnei  22363  fcfelbas  22364  cnpfcf  22369  cnfcf  22370  alexsublem  22372  tmdcn2  22417  tmdgsum  22423  tmdgsum2  22424  symgtgp  22429  subgntr  22434  opnsubg  22435  clssubg  22436  clsnsg  22437  cldsubg  22438  tgpconncompeqg  22439  tgpconncomp  22440  ghmcnp  22442  snclseqg  22443  tgphaus  22444  tgpt1  22445  prdstmdd  22451  prdstgpd  22452  tsmsgsum  22466  tsmsid  22467  tsmsmhm  22473  tsmsadd  22474  tgptsmscld  22478  utop3cls  22579  mopnuni  22770  isxms2  22777  prdsxmslem2  22858  metdseq0  23181  cnmpopc  23251  ishtpy  23295  om1val  23353  pi1val  23360  csscld  23571  clsocv  23572  cfilfcls  23596  relcmpcmet  23640  limcres  24203  limccnp  24208  limccnp2  24209  dvbss  24218  perfdvf  24220  dvreslem  24226  dvres2lem  24227  dvcnp2  24236  dvaddbr  24254  dvmulbr  24255  dvcmulf  24261  dvmptres2  24278  dvmptcmul  24280  dvmptntr  24287  dvcnvrelem2  24334  ftc1cn  24359  taylthlem1  24680  ulmdvlem3  24709  efrlim  25265  pl1cn  30875  cvxpconn  32107  cvxsconn  32108  ivthALT  33237  neibastop2  33263  neibastop3  33264  topmeet  33266  topjoin  33267  refsum2cnlem1  40747  dvresntr  41662  rrxunitopnfi  42038