Theorem toponuni 22830

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  ∪ cuni 4859  ‘cfv 6481  Topctop 22809  TopOnctopon 22826

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 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668

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 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-iota 6437  df-fun 6483  df-fv 6489  df-topon 22827

This theorem is referenced by:  toponunii  22832  toponmax  22842  toponss  22843  toponcom  22844  topgele  22846  topontopn  22856  toponmre  23009  cldmreon  23010  restuni  23078  resttopon2  23084  restlp  23099  restperf  23100  perfopn  23101  ordtcld1  23113  ordtcld2  23114  lmfval  23148  cnfval  23149  cnpfval  23150  cnpf2  23166  cnprcl2  23167  ssidcn  23171  iscnp4  23179  iscncl  23185  cncls2  23189  cncls  23190  cnntr  23191  cncnp  23196  lmcls  23218  lmcld  23219  iscnrm2  23254  ist0-2  23260  ist1-2  23263  ishaus2  23267  isreg2  23293  ordtt1  23295  sscmp  23321  dfconn2  23335  clsconn  23346  conncompcld  23350  1stccnp  23378  locfincf  23447  kgenval  23451  kgenuni  23455  1stckgenlem  23469  kgen2ss  23471  kgencn2  23473  txtopon  23507  txuni  23508  pttopon  23512  ptuniconst  23514  txcls  23520  ptclsg  23531  dfac14lem  23533  xkoccn  23535  ptcnplem  23537  ptcn  23543  cnmpt1t  23581  cnmpt2t  23589  cnmpt1res  23592  cnmpt2res  23593  cnmptkp  23596  cnmptk1p  23601  cnmptk2  23602  xkoinjcn  23603  elqtop3  23619  qtoptopon  23620  qtopcld  23629  qtoprest  23633  qtopcmap  23635  kqval  23642  kqcldsat  23649  isr0  23653  r0cld  23654  regr1lem  23655  kqnrmlem1  23659  kqnrmlem2  23660  pt1hmeo  23722  xpstopnlem1  23725  neifil  23796  trnei  23808  elflim  23887  flimss2  23888  flimss1  23889  flimopn  23891  fbflim2  23893  flimclslem  23900  flffval  23905  flfnei  23907  cnpflf2  23916  cnflf  23918  cnflf2  23919  isfcls2  23929  fclsopn  23930  fclsnei  23935  fclscmp  23946  ufilcmp  23948  fcfval  23949  fcfnei  23951  fcfelbas  23952  cnpfcf  23957  cnfcf  23958  alexsublem  23960  tmdcn2  24005  tmdgsum  24011  tmdgsum2  24012  symgtgp  24022  subgntr  24023  opnsubg  24024  clssubg  24025  clsnsg  24026  cldsubg  24027  tgpconncompeqg  24028  tgpconncomp  24029  ghmcnp  24031  snclseqg  24032  tgphaus  24033  tgpt1  24034  prdstmdd  24040  prdstgpd  24041  tsmsgsum  24055  tsmsid  24056  tsmsmhm  24062  tsmsadd  24063  tgptsmscld  24067  utop3cls  24167  mopnuni  24357  isxms2  24364  prdsxmslem2  24445  metdseq0  24771  cnmpopc  24850  ishtpy  24899  om1val  24958  pi1val  24965  csscld  25177  clsocv  25178  cfilfcls  25202  relcmpcmet  25246  limcres  25815  limccnp  25820  limccnp2  25821  dvbss  25830  perfdvf  25832  dvreslem  25838  dvres2lem  25839  dvcnp2  25849  dvcnp2OLD  25850  dvaddbr  25868  dvmulbr  25869  dvmulbrOLD  25870  dvcmulf  25876  dvmptres2  25894  dvmptcmul  25896  dvmptntr  25903  dvcnvrelem2  25951  ftc1cn  25978  taylthlem1  26309  ulmdvlem3  26339  efrlim  26907  efrlimOLD  26908  zart0  33890  zarmxt1  33891  pl1cn  33966  cvxpconn  35284  cvxsconn  35285  ivthALT  36375  neibastop2  36401  neibastop3  36402  topmeet  36404  topjoin  36405  refsum2cnlem1  45080  dvresntr  45962  rrxunitopnfi  46336