Theorem toponuni 20642

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

Syntax hints:   → wi 4   = wceq 1480   ∈ wcel 1987  ∪ cuni 4402  ‘cfv 5847  Topctop 20617  TopOnctopon 20618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-iota 5810  df-fun 5849  df-fv 5855  df-topon 20623

This theorem is referenced by:  toponmax  20643  toponss  20644  toponcom  20645  toponunii  20647  topgele  20649  topontopn  20657  toponmre  20807  cldmreon  20808  restuni  20876  resttopon2  20882  restlp  20897  restperf  20898  perfopn  20899  ordtcld1  20911  ordtcld2  20912  lmfval  20946  cnfval  20947  cnpfval  20948  cnpf2  20964  cnprcl2  20965  ssidcn  20969  iscnp4  20977  iscncl  20983  cncls2  20987  cncls  20988  cnntr  20989  cncnp  20994  lmcls  21016  lmcld  21017  iscnrm2  21052  ist0-2  21058  ist1-2  21061  ishaus2  21065  isreg2  21091  ordtt1  21093  sscmp  21118  dfconn2  21132  clsconn  21143  conncompcld  21147  1stccnp  21175  locfincf  21244  kgenval  21248  kgenuni  21252  1stckgenlem  21266  kgen2ss  21268  kgencn2  21270  txtopon  21304  txuni  21305  pttopon  21309  ptuniconst  21311  txcls  21317  ptclsg  21328  dfac14lem  21330  xkoccn  21332  ptcnplem  21334  ptcn  21340  cnmpt1t  21378  cnmpt2t  21386  cnmpt1res  21389  cnmpt2res  21390  cnmptkp  21393  cnmptk1p  21398  cnmptk2  21399  xkoinjcn  21400  elqtop3  21416  qtoptopon  21417  qtopcld  21426  qtoprest  21430  qtopcmap  21432  kqval  21439  kqcldsat  21446  isr0  21450  r0cld  21451  regr1lem  21452  kqnrmlem1  21456  kqnrmlem2  21457  pt1hmeo  21519  xpstopnlem1  21522  neifil  21594  trnei  21606  elflim  21685  flimss2  21686  flimss1  21687  flimopn  21689  fbflim2  21691  flimclslem  21698  flffval  21703  flfnei  21705  cnpflf2  21714  cnflf  21716  cnflf2  21717  isfcls2  21727  fclsopn  21728  fclsnei  21733  fclscmp  21744  ufilcmp  21746  fcfval  21747  fcfnei  21749  fcfelbas  21750  cnpfcf  21755  cnfcf  21756  alexsublem  21758  tmdcn2  21803  tmdgsum  21809  tmdgsum2  21810  symgtgp  21815  subgntr  21820  opnsubg  21821  clssubg  21822  clsnsg  21823  cldsubg  21824  tgpconncompeqg  21825  tgpconncomp  21826  ghmcnp  21828  snclseqg  21829  tgphaus  21830  tgpt1  21831  prdstmdd  21837  prdstgpd  21838  tsmsgsum  21852  tsmsid  21853  tsmsmhm  21859  tsmsadd  21860  tgptsmscld  21864  utop3cls  21965  mopnuni  22156  isxms2  22163  prdsxmslem2  22244  metdseq0  22565  cnmpt2pc  22635  ishtpy  22679  om1val  22738  pi1val  22745  csscld  22956  clsocv  22957  cfilfcls  22980  relcmpcmet  23023  limcres  23556  limccnp  23561  limccnp2  23562  dvbss  23571  perfdvf  23573  dvreslem  23579  dvres2lem  23580  dvcnp2  23589  dvaddbr  23607  dvmulbr  23608  dvcmulf  23614  dvmptres2  23631  dvmptcmul  23633  dvmptntr  23640  dvcnvrelem2  23685  ftc1cn  23710  taylthlem1  24031  ulmdvlem3  24060  efrlim  24596  pl1cn  29783  cvxpconn  30932  cvxsconn  30933  ivthALT  31972  neibastop2  31998  neibastop3  31999  topmeet  32001  topjoin  32002  refsum2cnlem1  38679  dvresntr  39437  rrxunitopnfi  39819