Theorem toponuni 22832

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ∪ cuni 4860  ‘cfv 6488  Topctop 22811  TopOnctopon 22828

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7676

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-iota 6444  df-fun 6490  df-fv 6496  df-topon 22829

This theorem is referenced by:  toponunii  22834  toponmax  22844  toponss  22845  toponcom  22846  topgele  22848  topontopn  22858  toponmre  23011  cldmreon  23012  restuni  23080  resttopon2  23086  restlp  23101  restperf  23102  perfopn  23103  ordtcld1  23115  ordtcld2  23116  lmfval  23150  cnfval  23151  cnpfval  23152  cnpf2  23168  cnprcl2  23169  ssidcn  23173  iscnp4  23181  iscncl  23187  cncls2  23191  cncls  23192  cnntr  23193  cncnp  23198  lmcls  23220  lmcld  23221  iscnrm2  23256  ist0-2  23262  ist1-2  23265  ishaus2  23269  isreg2  23295  ordtt1  23297  sscmp  23323  dfconn2  23337  clsconn  23348  conncompcld  23352  1stccnp  23380  locfincf  23449  kgenval  23453  kgenuni  23457  1stckgenlem  23471  kgen2ss  23473  kgencn2  23475  txtopon  23509  txuni  23510  pttopon  23514  ptuniconst  23516  txcls  23522  ptclsg  23533  dfac14lem  23535  xkoccn  23537  ptcnplem  23539  ptcn  23545  cnmpt1t  23583  cnmpt2t  23591  cnmpt1res  23594  cnmpt2res  23595  cnmptkp  23598  cnmptk1p  23603  cnmptk2  23604  xkoinjcn  23605  elqtop3  23621  qtoptopon  23622  qtopcld  23631  qtoprest  23635  qtopcmap  23637  kqval  23644  kqcldsat  23651  isr0  23655  r0cld  23656  regr1lem  23657  kqnrmlem1  23661  kqnrmlem2  23662  pt1hmeo  23724  xpstopnlem1  23727  neifil  23798  trnei  23810  elflim  23889  flimss2  23890  flimss1  23891  flimopn  23893  fbflim2  23895  flimclslem  23902  flffval  23907  flfnei  23909  cnpflf2  23918  cnflf  23920  cnflf2  23921  isfcls2  23931  fclsopn  23932  fclsnei  23937  fclscmp  23948  ufilcmp  23950  fcfval  23951  fcfnei  23953  fcfelbas  23954  cnpfcf  23959  cnfcf  23960  alexsublem  23962  tmdcn2  24007  tmdgsum  24013  tmdgsum2  24014  symgtgp  24024  subgntr  24025  opnsubg  24026  clssubg  24027  clsnsg  24028  cldsubg  24029  tgpconncompeqg  24030  tgpconncomp  24031  ghmcnp  24033  snclseqg  24034  tgphaus  24035  tgpt1  24036  prdstmdd  24042  prdstgpd  24043  tsmsgsum  24057  tsmsid  24058  tsmsmhm  24064  tsmsadd  24065  tgptsmscld  24069  utop3cls  24169  mopnuni  24359  isxms2  24366  prdsxmslem2  24447  metdseq0  24773  cnmpopc  24852  ishtpy  24901  om1val  24960  pi1val  24967  csscld  25179  clsocv  25180  cfilfcls  25204  relcmpcmet  25248  limcres  25817  limccnp  25822  limccnp2  25823  dvbss  25832  perfdvf  25834  dvreslem  25840  dvres2lem  25841  dvcnp2  25851  dvcnp2OLD  25852  dvaddbr  25870  dvmulbr  25871  dvmulbrOLD  25872  dvcmulf  25878  dvmptres2  25896  dvmptcmul  25898  dvmptntr  25905  dvcnvrelem2  25953  ftc1cn  25980  taylthlem1  26311  ulmdvlem3  26341  efrlim  26909  efrlimOLD  26910  zart0  33915  zarmxt1  33916  pl1cn  33991  cvxpconn  35309  cvxsconn  35310  ivthALT  36402  neibastop2  36428  neibastop3  36429  topmeet  36431  topjoin  36432  refsum2cnlem1  45161  dvresntr  46043  rrxunitopnfi  46417