Theorem toponuni 22870

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  ∪ cuni 4865  ‘cfv 6500  Topctop 22849  TopOnctopon 22866

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fv 6508  df-topon 22867

This theorem is referenced by:  toponunii  22872  toponmax  22882  toponss  22883  toponcom  22884  topgele  22886  topontopn  22896  toponmre  23049  cldmreon  23050  restuni  23118  resttopon2  23124  restlp  23139  restperf  23140  perfopn  23141  ordtcld1  23153  ordtcld2  23154  lmfval  23188  cnfval  23189  cnpfval  23190  cnpf2  23206  cnprcl2  23207  ssidcn  23211  iscnp4  23219  iscncl  23225  cncls2  23229  cncls  23230  cnntr  23231  cncnp  23236  lmcls  23258  lmcld  23259  iscnrm2  23294  ist0-2  23300  ist1-2  23303  ishaus2  23307  isreg2  23333  ordtt1  23335  sscmp  23361  dfconn2  23375  clsconn  23386  conncompcld  23390  1stccnp  23418  locfincf  23487  kgenval  23491  kgenuni  23495  1stckgenlem  23509  kgen2ss  23511  kgencn2  23513  txtopon  23547  txuni  23548  pttopon  23552  ptuniconst  23554  txcls  23560  ptclsg  23571  dfac14lem  23573  xkoccn  23575  ptcnplem  23577  ptcn  23583  cnmpt1t  23621  cnmpt2t  23629  cnmpt1res  23632  cnmpt2res  23633  cnmptkp  23636  cnmptk1p  23641  cnmptk2  23642  xkoinjcn  23643  elqtop3  23659  qtoptopon  23660  qtopcld  23669  qtoprest  23673  qtopcmap  23675  kqval  23682  kqcldsat  23689  isr0  23693  r0cld  23694  regr1lem  23695  kqnrmlem1  23699  kqnrmlem2  23700  pt1hmeo  23762  xpstopnlem1  23765  neifil  23836  trnei  23848  elflim  23927  flimss2  23928  flimss1  23929  flimopn  23931  fbflim2  23933  flimclslem  23940  flffval  23945  flfnei  23947  cnpflf2  23956  cnflf  23958  cnflf2  23959  isfcls2  23969  fclsopn  23970  fclsnei  23975  fclscmp  23986  ufilcmp  23988  fcfval  23989  fcfnei  23991  fcfelbas  23992  cnpfcf  23997  cnfcf  23998  alexsublem  24000  tmdcn2  24045  tmdgsum  24051  tmdgsum2  24052  symgtgp  24062  subgntr  24063  opnsubg  24064  clssubg  24065  clsnsg  24066  cldsubg  24067  tgpconncompeqg  24068  tgpconncomp  24069  ghmcnp  24071  snclseqg  24072  tgphaus  24073  tgpt1  24074  prdstmdd  24080  prdstgpd  24081  tsmsgsum  24095  tsmsid  24096  tsmsmhm  24102  tsmsadd  24103  tgptsmscld  24107  utop3cls  24207  mopnuni  24397  isxms2  24404  prdsxmslem2  24485  metdseq0  24811  cnmpopc  24890  ishtpy  24939  om1val  24998  pi1val  25005  csscld  25217  clsocv  25218  cfilfcls  25242  relcmpcmet  25286  limcres  25855  limccnp  25860  limccnp2  25861  dvbss  25870  perfdvf  25872  dvreslem  25878  dvres2lem  25879  dvcnp2  25889  dvcnp2OLD  25890  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmulf  25916  dvmptres2  25934  dvmptcmul  25936  dvmptntr  25943  dvcnvrelem2  25991  ftc1cn  26018  taylthlem1  26349  ulmdvlem3  26379  efrlim  26947  efrlimOLD  26948  zart0  34056  zarmxt1  34057  pl1cn  34132  cvxpconn  35455  cvxsconn  35456  ivthALT  36548  neibastop2  36574  neibastop3  36575  topmeet  36577  topjoin  36578  refsum2cnlem1  45394  dvresntr  46273  rrxunitopnfi  46647