Theorem toponuni 23028

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6525  Topctop 23007  TopOnctopon 23024

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2737  ax-sep 5250  ax-nul 5260  ax-pow 5326  ax-pr 5394  ax-un 7722

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-nf 1807  df-sb 2094  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-pw 4560  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5105  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6481  df-fun 6527  df-fv 6533  df-topon 23025

This theorem is referenced by:  toponunii  23030  toponmax  23040  toponss  23041  toponcom  23042  topgele  23044  topontopn  23054  toponmre  23207  cldmreon  23208  restuni  23276  resttopon2  23282  restlp  23297  restperf  23298  perfopn  23299  ordtcld1  23311  ordtcld2  23312  lmfval  23346  cnfval  23347  cnpfval  23348  cnpf2  23364  cnprcl2  23365  ssidcn  23369  iscnp4  23377  iscncl  23383  cncls2  23387  cncls  23388  cnntr  23389  cncnp  23394  lmcls  23416  lmcld  23417  iscnrm2  23452  ist0-2  23458  ist1-2  23461  ishaus2  23465  isreg2  23491  ordtt1  23493  sscmp  23519  dfconn2  23533  clsconn  23544  conncompcld  23548  1stccnp  23576  locfincf  23645  kgenval  23649  kgenuni  23653  1stckgenlem  23667  kgen2ss  23669  kgencn2  23671  txtopon  23705  txuni  23706  pttopon  23710  ptuniconst  23712  txcls  23718  ptclsg  23729  dfac14lem  23731  xkoccn  23733  ptcnplem  23735  ptcn  23741  cnmpt1t  23779  cnmpt2t  23787  cnmpt1res  23790  cnmpt2res  23791  cnmptkp  23794  cnmptk1p  23799  cnmptk2  23800  xkoinjcn  23801  elqtop3  23817  qtoptopon  23818  qtopcld  23827  qtoprest  23831  qtopcmap  23833  kqval  23840  kqcldsat  23847  isr0  23851  r0cld  23852  regr1lem  23853  kqnrmlem1  23857  kqnrmlem2  23858  pt1hmeo  23920  xpstopnlem1  23923  neifil  23994  trnei  24006  elflim  24085  flimss2  24086  flimss1  24087  flimopn  24089  fbflim2  24091  flimclslem  24098  flffval  24103  flfnei  24105  cnpflf2  24114  cnflf  24116  cnflf2  24117  isfcls2  24127  fclsopn  24128  fclsnei  24133  fclscmp  24144  ufilcmp  24146  fcfval  24147  fcfnei  24149  fcfelbas  24150  cnpfcf  24155  cnfcf  24156  alexsublem  24158  tmdcn2  24203  tmdgsum  24209  tmdgsum2  24210  symgtgp  24220  subgntr  24221  opnsubg  24222  clssubg  24223  clsnsg  24224  cldsubg  24225  tgpconncompeqg  24226  tgpconncomp  24227  ghmcnp  24229  snclseqg  24230  tgphaus  24231  tgpt1  24232  prdstmdd  24238  prdstgpd  24239  tsmsgsum  24253  tsmsid  24254  tsmsmhm  24260  tsmsadd  24261  tgptsmscld  24265  utop3cls  24365  mopnuni  24555  isxms2  24562  prdsxmslem2  24643  metdseq0  24969  cnmpopc  25044  ishtpy  25088  om1val  25146  pi1val  25153  csscld  25365  clsocv  25366  cfilfcls  25390  relcmpcmet  25434  limcres  26002  limccnp  26007  limccnp2  26008  dvbss  26017  perfdvf  26019  dvreslem  26025  dvres2lem  26026  dvcnp2  26036  dvaddbr  26054  dvmulbr  26055  dvcmulf  26061  dvmptres2  26078  dvmptcmul  26080  dvmptntr  26087  dvcnvrelem2  26134  ftc1cn  26159  taylthlem1  26490  ulmdvlem3  26519  efrlim  27088  zart0  34181  zarmxt1  34182  pl1cn  34257  cvxpconn  35600  cvxsconn  35601  ivthALT  36703  neibastop2  36729  neibastop3  36730  topmeet  36732  topjoin  36733  refsum2cnlem1  45616  dvresntr  46491  rrxunitopnfi  46865