Theorem toponuni 20921

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

Syntax hints:   → wi 4   = wceq 1632   ∈ wcel 2139  ∪ cuni 4588  ‘cfv 6049  Topctop 20900  TopOnctopon 20917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fv 6057  df-topon 20918

This theorem is referenced by:  toponunii  20923  toponmax  20932  toponss  20933  toponcom  20934  topgele  20936  topontopn  20946  toponmre  21099  cldmreon  21100  restuni  21168  resttopon2  21174  restlp  21189  restperf  21190  perfopn  21191  ordtcld1  21203  ordtcld2  21204  lmfval  21238  cnfval  21239  cnpfval  21240  cnpf2  21256  cnprcl2  21257  ssidcn  21261  iscnp4  21269  iscncl  21275  cncls2  21279  cncls  21280  cnntr  21281  cncnp  21286  lmcls  21308  lmcld  21309  iscnrm2  21344  ist0-2  21350  ist1-2  21353  ishaus2  21357  isreg2  21383  ordtt1  21385  sscmp  21410  dfconn2  21424  clsconn  21435  conncompcld  21439  1stccnp  21467  locfincf  21536  kgenval  21540  kgenuni  21544  1stckgenlem  21558  kgen2ss  21560  kgencn2  21562  txtopon  21596  txuni  21597  pttopon  21601  ptuniconst  21603  txcls  21609  ptclsg  21620  dfac14lem  21622  xkoccn  21624  ptcnplem  21626  ptcn  21632  cnmpt1t  21670  cnmpt2t  21678  cnmpt1res  21681  cnmpt2res  21682  cnmptkp  21685  cnmptk1p  21690  cnmptk2  21691  xkoinjcn  21692  elqtop3  21708  qtoptopon  21709  qtopcld  21718  qtoprest  21722  qtopcmap  21724  kqval  21731  kqcldsat  21738  isr0  21742  r0cld  21743  regr1lem  21744  kqnrmlem1  21748  kqnrmlem2  21749  pt1hmeo  21811  xpstopnlem1  21814  neifil  21885  trnei  21897  elflim  21976  flimss2  21977  flimss1  21978  flimopn  21980  fbflim2  21982  flimclslem  21989  flffval  21994  flfnei  21996  cnpflf2  22005  cnflf  22007  cnflf2  22008  isfcls2  22018  fclsopn  22019  fclsnei  22024  fclscmp  22035  ufilcmp  22037  fcfval  22038  fcfnei  22040  fcfelbas  22041  cnpfcf  22046  cnfcf  22047  alexsublem  22049  tmdcn2  22094  tmdgsum  22100  tmdgsum2  22101  symgtgp  22106  subgntr  22111  opnsubg  22112  clssubg  22113  clsnsg  22114  cldsubg  22115  tgpconncompeqg  22116  tgpconncomp  22117  ghmcnp  22119  snclseqg  22120  tgphaus  22121  tgpt1  22122  prdstmdd  22128  prdstgpd  22129  tsmsgsum  22143  tsmsid  22144  tsmsmhm  22150  tsmsadd  22151  tgptsmscld  22155  utop3cls  22256  mopnuni  22447  isxms2  22454  prdsxmslem2  22535  metdseq0  22858  cnmpt2pc  22928  ishtpy  22972  om1val  23030  pi1val  23037  csscld  23248  clsocv  23249  cfilfcls  23272  relcmpcmet  23315  limcres  23849  limccnp  23854  limccnp2  23855  dvbss  23864  perfdvf  23866  dvreslem  23872  dvres2lem  23873  dvcnp2  23882  dvaddbr  23900  dvmulbr  23901  dvcmulf  23907  dvmptres2  23924  dvmptcmul  23926  dvmptntr  23933  dvcnvrelem2  23980  ftc1cn  24005  taylthlem1  24326  ulmdvlem3  24355  efrlim  24895  pl1cn  30310  cvxpconn  31531  cvxsconn  31532  ivthALT  32636  neibastop2  32662  neibastop3  32663  topmeet  32665  topjoin  32666  refsum2cnlem1  39695  dvresntr  40635  rrxunitopnfi  41015