Theorem toponuni 23212

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∪ cuni 4867  ‘cfv 6531  Topctop 23191  TopOnctopon 23208

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6487  df-fun 6533  df-fv 6539  df-topon 23209

This theorem is used by:  toponunii  23214  toponmax  23224  toponss  23225  toponcom  23226  topgele  23228  topontopn  23238  toponmre  23391  cldmreon  23392  restuni  23460  resttopon2  23466  restlp  23481  restperf  23482  perfopn  23483  ordtcld1  23495  ordtcld2  23496  lmfval  23530  cnfval  23531  cnpfval  23532  cnpf2  23548  cnprcl2  23549  ssidcn  23553  iscnp4  23561  iscncl  23567  cncls2  23571  cncls  23572  cnntr  23573  cncnp  23578  lmcls  23600  lmcld  23601  iscnrm2  23636  ist0-2  23642  ist1-2  23645  ishaus2  23649  isreg2  23675  ordtt1  23677  sscmp  23703  dfconn2  23717  clsconn  23728  conncompcld  23732  1stccnp  23761  locfincf  23830  kgenval  23834  kgenuni  23838  1stckgenlem  23852  kgen2ss  23854  kgencn2  23856  txtopon  23890  txuni  23891  pttopon  23895  ptuniconst  23897  txcls  23903  ptclsg  23914  dfac14lem  23916  xkoccn  23918  ptcnplem  23920  ptcn  23926  cnmpt1t  23964  cnmpt2t  23972  cnmpt1res  23975  cnmpt2res  23976  cnmptkp  23979  cnmptk1p  23984  cnmptk2  23985  xkoinjcn  23986  elqtop3  24002  qtoptopon  24003  qtopcld  24012  qtoprest  24016  qtopcmap  24018  kqval  24025  kqcldsat  24032  isr0  24036  r0cld  24037  regr1lem  24038  kqnrmlem1  24042  kqnrmlem2  24043  pt1hmeo  24105  xpstopnlem1  24108  neifil  24179  trnei  24191  elflim  24270  flimss2  24271  flimss1  24272  flimopn  24274  fbflim2  24276  flimclslem  24283  flffval  24288  flfnei  24290  cnpflf2  24299  cnflf  24301  cnflf2  24302  isfcls2  24312  fclsopn  24313  fclsnei  24318  fclscmp  24329  ufilcmp  24331  fcfval  24332  fcfnei  24334  fcfelbas  24335  cnpfcf  24340  cnfcf  24341  alexsublem  24343  tmdcn2  24388  tmdgsum  24394  tmdgsum2  24395  symgtgp  24405  subgntr  24406  opnsubg  24407  clssubg  24408  clsnsg  24409  cldsubg  24410  tgpconncompeqg  24411  tgpconncomp  24412  ghmcnp  24414  snclseqg  24415  tgphaus  24416  tgpt1  24417  prdstmdd  24423  prdstgpd  24424  tsmsgsum  24438  tsmsid  24439  tsmsmhm  24445  tsmsadd  24446  tgptsmscld  24450  utop3cls  24550  mopnuni  24740  isxms2  24747  prdsxmslem2  24828  metdseq0  25154  cnmpopc  25229  ishtpy  25273  om1val  25331  pi1val  25338  csscld  25550  clsocv  25551  cfilfcls  25575  relcmpcmet  25619  limcres  26186  limccnp  26191  limccnp2  26192  dvbss  26201  perfdvf  26203  dvreslem  26209  dvres2lem  26210  dvcnp2  26220  dvaddbr  26238  dvmulbr  26239  dvcmulf  26245  dvmptres2  26262  dvmptcmul  26264  dvmptntr  26271  dvcnvrelem2  26318  ftc1cn  26343  taylthlem1  26682  ulmdvlem3  26711  efrlim  27279  zart0  34493  zarmxt1  34494  pl1cn  34569  cvxpconn  35976  cvxsconn  35977  ivthALT  37093  neibastop2  37119  neibastop3  37120  topmeet  37122  topjoin  37123  refsum2cnlem1  45997  dvresntr  46872  rrxunitopnfi  47246