Theorem toponuni 22300

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2106  ∪ cuni 4870  ‘cfv 6501  Topctop 22279  TopOnctopon 22296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-iota 6453  df-fun 6503  df-fv 6509  df-topon 22297

This theorem is referenced by:  toponunii  22302  toponmax  22312  toponss  22313  toponcom  22314  topgele  22316  topontopn  22326  toponmre  22481  cldmreon  22482  restuni  22550  resttopon2  22556  restlp  22571  restperf  22572  perfopn  22573  ordtcld1  22585  ordtcld2  22586  lmfval  22620  cnfval  22621  cnpfval  22622  cnpf2  22638  cnprcl2  22639  ssidcn  22643  iscnp4  22651  iscncl  22657  cncls2  22661  cncls  22662  cnntr  22663  cncnp  22668  lmcls  22690  lmcld  22691  iscnrm2  22726  ist0-2  22732  ist1-2  22735  ishaus2  22739  isreg2  22765  ordtt1  22767  sscmp  22793  dfconn2  22807  clsconn  22818  conncompcld  22822  1stccnp  22850  locfincf  22919  kgenval  22923  kgenuni  22927  1stckgenlem  22941  kgen2ss  22943  kgencn2  22945  txtopon  22979  txuni  22980  pttopon  22984  ptuniconst  22986  txcls  22992  ptclsg  23003  dfac14lem  23005  xkoccn  23007  ptcnplem  23009  ptcn  23015  cnmpt1t  23053  cnmpt2t  23061  cnmpt1res  23064  cnmpt2res  23065  cnmptkp  23068  cnmptk1p  23073  cnmptk2  23074  xkoinjcn  23075  elqtop3  23091  qtoptopon  23092  qtopcld  23101  qtoprest  23105  qtopcmap  23107  kqval  23114  kqcldsat  23121  isr0  23125  r0cld  23126  regr1lem  23127  kqnrmlem1  23131  kqnrmlem2  23132  pt1hmeo  23194  xpstopnlem1  23197  neifil  23268  trnei  23280  elflim  23359  flimss2  23360  flimss1  23361  flimopn  23363  fbflim2  23365  flimclslem  23372  flffval  23377  flfnei  23379  cnpflf2  23388  cnflf  23390  cnflf2  23391  isfcls2  23401  fclsopn  23402  fclsnei  23407  fclscmp  23418  ufilcmp  23420  fcfval  23421  fcfnei  23423  fcfelbas  23424  cnpfcf  23429  cnfcf  23430  alexsublem  23432  tmdcn2  23477  tmdgsum  23483  tmdgsum2  23484  symgtgp  23494  subgntr  23495  opnsubg  23496  clssubg  23497  clsnsg  23498  cldsubg  23499  tgpconncompeqg  23500  tgpconncomp  23501  ghmcnp  23503  snclseqg  23504  tgphaus  23505  tgpt1  23506  prdstmdd  23512  prdstgpd  23513  tsmsgsum  23527  tsmsid  23528  tsmsmhm  23534  tsmsadd  23535  tgptsmscld  23539  utop3cls  23640  mopnuni  23831  isxms2  23838  prdsxmslem2  23922  metdseq0  24254  cnmpopc  24328  ishtpy  24372  om1val  24430  pi1val  24437  csscld  24650  clsocv  24651  cfilfcls  24675  relcmpcmet  24719  limcres  25287  limccnp  25292  limccnp2  25293  dvbss  25302  perfdvf  25304  dvreslem  25310  dvres2lem  25311  dvcnp2  25321  dvaddbr  25339  dvmulbr  25340  dvcmulf  25346  dvmptres2  25363  dvmptcmul  25365  dvmptntr  25372  dvcnvrelem2  25419  ftc1cn  25444  taylthlem1  25769  ulmdvlem3  25798  efrlim  26356  zart0  32549  zarmxt1  32550  pl1cn  32625  cvxpconn  33923  cvxsconn  33924  ivthALT  34883  neibastop2  34909  neibastop3  34910  topmeet  34912  topjoin  34913  refsum2cnlem1  43364  dvresntr  44279  rrxunitopnfi  44653