Theorem toponuni 23145

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∪ cuni 4870  ‘cfv 6537  Topctop 23124  TopOnctopon 23141

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 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  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 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6493  df-fun 6539  df-fv 6545  df-topon 23142

This theorem is used by:  toponunii  23147  toponmax  23157  toponss  23158  toponcom  23159  topgele  23161  topontopn  23171  toponmre  23324  cldmreon  23325  restuni  23393  resttopon2  23399  restlp  23414  restperf  23415  perfopn  23416  ordtcld1  23428  ordtcld2  23429  lmfval  23463  cnfval  23464  cnpfval  23465  cnpf2  23481  cnprcl2  23482  ssidcn  23486  iscnp4  23494  iscncl  23500  cncls2  23504  cncls  23505  cnntr  23506  cncnp  23511  lmcls  23533  lmcld  23534  iscnrm2  23569  ist0-2  23575  ist1-2  23578  ishaus2  23582  isreg2  23608  ordtt1  23610  sscmp  23636  dfconn2  23650  clsconn  23661  conncompcld  23665  1stccnp  23694  locfincf  23763  kgenval  23767  kgenuni  23771  1stckgenlem  23785  kgen2ss  23787  kgencn2  23789  txtopon  23823  txuni  23824  pttopon  23828  ptuniconst  23830  txcls  23836  ptclsg  23847  dfac14lem  23849  xkoccn  23851  ptcnplem  23853  ptcn  23859  cnmpt1t  23897  cnmpt2t  23905  cnmpt1res  23908  cnmpt2res  23909  cnmptkp  23912  cnmptk1p  23917  cnmptk2  23918  xkoinjcn  23919  elqtop3  23935  qtoptopon  23936  qtopcld  23945  qtoprest  23949  qtopcmap  23951  kqval  23958  kqcldsat  23965  isr0  23969  r0cld  23970  regr1lem  23971  kqnrmlem1  23975  kqnrmlem2  23976  pt1hmeo  24038  xpstopnlem1  24041  neifil  24112  trnei  24124  elflim  24203  flimss2  24204  flimss1  24205  flimopn  24207  fbflim2  24209  flimclslem  24216  flffval  24221  flfnei  24223  cnpflf2  24232  cnflf  24234  cnflf2  24235  isfcls2  24245  fclsopn  24246  fclsnei  24251  fclscmp  24262  ufilcmp  24264  fcfval  24265  fcfnei  24267  fcfelbas  24268  cnpfcf  24273  cnfcf  24274  alexsublem  24276  tmdcn2  24321  tmdgsum  24327  tmdgsum2  24328  symgtgp  24338  subgntr  24339  opnsubg  24340  clssubg  24341  clsnsg  24342  cldsubg  24343  tgpconncompeqg  24344  tgpconncomp  24345  ghmcnp  24347  snclseqg  24348  tgphaus  24349  tgpt1  24350  prdstmdd  24356  prdstgpd  24357  tsmsgsum  24371  tsmsid  24372  tsmsmhm  24378  tsmsadd  24379  tgptsmscld  24383  utop3cls  24483  mopnuni  24673  isxms2  24680  prdsxmslem2  24761  metdseq0  25087  cnmpopc  25162  ishtpy  25206  om1val  25264  pi1val  25271  csscld  25483  clsocv  25484  cfilfcls  25508  relcmpcmet  25552  limcres  26120  limccnp  26125  limccnp2  26126  dvbss  26135  perfdvf  26137  dvreslem  26143  dvres2lem  26144  dvcnp2  26154  dvaddbr  26172  dvmulbr  26173  dvcmulf  26179  dvmptres2  26196  dvmptcmul  26198  dvmptntr  26205  dvcnvrelem2  26252  ftc1cn  26277  taylthlem1  26616  ulmdvlem3  26645  efrlim  27214  zart0  34397  zarmxt1  34398  pl1cn  34473  cvxpconn  35829  cvxsconn  35830  ivthALT  36962  neibastop2  36988  neibastop3  36989  topmeet  36991  topjoin  36992  refsum2cnlem1  45879  dvresntr  46754  rrxunitopnfi  47128