Theorem toponuni 22801

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  ∪ cuni 4871  ‘cfv 6511  Topctop 22780  TopOnctopon 22797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6464  df-fun 6513  df-fv 6519  df-topon 22798

This theorem is referenced by:  toponunii  22803  toponmax  22813  toponss  22814  toponcom  22815  topgele  22817  topontopn  22827  toponmre  22980  cldmreon  22981  restuni  23049  resttopon2  23055  restlp  23070  restperf  23071  perfopn  23072  ordtcld1  23084  ordtcld2  23085  lmfval  23119  cnfval  23120  cnpfval  23121  cnpf2  23137  cnprcl2  23138  ssidcn  23142  iscnp4  23150  iscncl  23156  cncls2  23160  cncls  23161  cnntr  23162  cncnp  23167  lmcls  23189  lmcld  23190  iscnrm2  23225  ist0-2  23231  ist1-2  23234  ishaus2  23238  isreg2  23264  ordtt1  23266  sscmp  23292  dfconn2  23306  clsconn  23317  conncompcld  23321  1stccnp  23349  locfincf  23418  kgenval  23422  kgenuni  23426  1stckgenlem  23440  kgen2ss  23442  kgencn2  23444  txtopon  23478  txuni  23479  pttopon  23483  ptuniconst  23485  txcls  23491  ptclsg  23502  dfac14lem  23504  xkoccn  23506  ptcnplem  23508  ptcn  23514  cnmpt1t  23552  cnmpt2t  23560  cnmpt1res  23563  cnmpt2res  23564  cnmptkp  23567  cnmptk1p  23572  cnmptk2  23573  xkoinjcn  23574  elqtop3  23590  qtoptopon  23591  qtopcld  23600  qtoprest  23604  qtopcmap  23606  kqval  23613  kqcldsat  23620  isr0  23624  r0cld  23625  regr1lem  23626  kqnrmlem1  23630  kqnrmlem2  23631  pt1hmeo  23693  xpstopnlem1  23696  neifil  23767  trnei  23779  elflim  23858  flimss2  23859  flimss1  23860  flimopn  23862  fbflim2  23864  flimclslem  23871  flffval  23876  flfnei  23878  cnpflf2  23887  cnflf  23889  cnflf2  23890  isfcls2  23900  fclsopn  23901  fclsnei  23906  fclscmp  23917  ufilcmp  23919  fcfval  23920  fcfnei  23922  fcfelbas  23923  cnpfcf  23928  cnfcf  23929  alexsublem  23931  tmdcn2  23976  tmdgsum  23982  tmdgsum2  23983  symgtgp  23993  subgntr  23994  opnsubg  23995  clssubg  23996  clsnsg  23997  cldsubg  23998  tgpconncompeqg  23999  tgpconncomp  24000  ghmcnp  24002  snclseqg  24003  tgphaus  24004  tgpt1  24005  prdstmdd  24011  prdstgpd  24012  tsmsgsum  24026  tsmsid  24027  tsmsmhm  24033  tsmsadd  24034  tgptsmscld  24038  utop3cls  24139  mopnuni  24329  isxms2  24336  prdsxmslem2  24417  metdseq0  24743  cnmpopc  24822  ishtpy  24871  om1val  24930  pi1val  24937  csscld  25149  clsocv  25150  cfilfcls  25174  relcmpcmet  25218  limcres  25787  limccnp  25792  limccnp2  25793  dvbss  25802  perfdvf  25804  dvreslem  25810  dvres2lem  25811  dvcnp2  25821  dvcnp2OLD  25822  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  dvcmulf  25848  dvmptres2  25866  dvmptcmul  25868  dvmptntr  25875  dvcnvrelem2  25923  ftc1cn  25950  taylthlem1  26281  ulmdvlem3  26311  efrlim  26879  efrlimOLD  26880  zart0  33869  zarmxt1  33870  pl1cn  33945  cvxpconn  35229  cvxsconn  35230  ivthALT  36323  neibastop2  36349  neibastop3  36350  topmeet  36352  topjoin  36353  refsum2cnlem1  45031  dvresntr  45916  rrxunitopnfi  46290