Theorem toponuni 20959

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

Syntax hints:   → wi 4   = wceq 1634   ∈ wcel 2148  ∪ cuni 4585  ‘cfv 6042  Topctop 20938  TopOnctopon 20955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3357  df-sbc 3594  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-pw 4309  df-sn 4327  df-pr 4329  df-op 4333  df-uni 4586  df-br 4798  df-opab 4860  df-mpt 4877  df-id 5171  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-iota 6005  df-fun 6044  df-fv 6050  df-topon 20956

This theorem is referenced by:  toponunii  20961  toponmax  20971  toponss  20972  toponcom  20973  topgele  20975  topontopn  20985  toponmre  21138  cldmreon  21139  restuni  21207  resttopon2  21213  restlp  21228  restperf  21229  perfopn  21230  ordtcld1  21242  ordtcld2  21243  lmfval  21277  cnfval  21278  cnpfval  21279  cnpf2  21295  cnprcl2  21296  ssidcn  21300  iscnp4  21308  iscncl  21314  cncls2  21318  cncls  21319  cnntr  21320  cncnp  21325  lmcls  21347  lmcld  21348  iscnrm2  21383  ist0-2  21389  ist1-2  21392  ishaus2  21396  isreg2  21422  ordtt1  21424  sscmp  21449  dfconn2  21463  clsconn  21474  conncompcld  21478  1stccnp  21506  locfincf  21575  kgenval  21579  kgenuni  21583  1stckgenlem  21597  kgen2ss  21599  kgencn2  21601  txtopon  21635  txuni  21636  pttopon  21640  ptuniconst  21642  txcls  21648  ptclsg  21659  dfac14lem  21661  xkoccn  21663  ptcnplem  21665  ptcn  21671  cnmpt1t  21709  cnmpt2t  21717  cnmpt1res  21720  cnmpt2res  21721  cnmptkp  21724  cnmptk1p  21729  cnmptk2  21730  xkoinjcn  21731  elqtop3  21747  qtoptopon  21748  qtopcld  21757  qtoprest  21761  qtopcmap  21763  kqval  21770  kqcldsat  21777  isr0  21781  r0cld  21782  regr1lem  21783  kqnrmlem1  21787  kqnrmlem2  21788  pt1hmeo  21850  xpstopnlem1  21853  neifil  21924  trnei  21936  elflim  22015  flimss2  22016  flimss1  22017  flimopn  22019  fbflim2  22021  flimclslem  22028  flffval  22033  flfnei  22035  cnpflf2  22044  cnflf  22046  cnflf2  22047  isfcls2  22057  fclsopn  22058  fclsnei  22063  fclscmp  22074  ufilcmp  22076  fcfval  22077  fcfnei  22079  fcfelbas  22080  cnpfcf  22085  cnfcf  22086  alexsublem  22088  tmdcn2  22133  tmdgsum  22139  tmdgsum2  22140  symgtgp  22145  subgntr  22150  opnsubg  22151  clssubg  22152  clsnsg  22153  cldsubg  22154  tgpconncompeqg  22155  tgpconncomp  22156  ghmcnp  22158  snclseqg  22159  tgphaus  22160  tgpt1  22161  prdstmdd  22167  prdstgpd  22168  tsmsgsum  22182  tsmsid  22183  tsmsmhm  22189  tsmsadd  22190  tgptsmscld  22194  utop3cls  22295  mopnuni  22486  isxms2  22493  prdsxmslem2  22574  metdseq0  22897  cnmpt2pc  22967  ishtpy  23011  om1val  23069  pi1val  23076  csscld  23287  clsocv  23288  cfilfcls  23311  relcmpcmet  23354  limcres  23891  limccnp  23896  limccnp2  23897  dvbss  23906  perfdvf  23908  dvreslem  23914  dvres2lem  23915  dvcnp2  23924  dvaddbr  23942  dvmulbr  23943  dvcmulf  23949  dvmptres2  23966  dvmptcmul  23968  dvmptntr  23975  dvcnvrelem2  24022  ftc1cn  24047  taylthlem1  24368  ulmdvlem3  24397  efrlim  24938  pl1cn  30358  cvxpconn  31579  cvxsconn  31580  ivthALT  32684  neibastop2  32710  neibastop3  32711  topmeet  32713  topjoin  32714  refsum2cnlem1  39730  dvresntr  40656  rrxunitopnfi  41035