Theorem toponuni 22935

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  ∪ cuni 4911  ‘cfv 6562  Topctop 22914  TopOnctopon 22931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fv 6570  df-topon 22932

This theorem is referenced by:  toponunii  22937  toponmax  22947  toponss  22948  toponcom  22949  topgele  22951  topontopn  22961  toponmre  23116  cldmreon  23117  restuni  23185  resttopon2  23191  restlp  23206  restperf  23207  perfopn  23208  ordtcld1  23220  ordtcld2  23221  lmfval  23255  cnfval  23256  cnpfval  23257  cnpf2  23273  cnprcl2  23274  ssidcn  23278  iscnp4  23286  iscncl  23292  cncls2  23296  cncls  23297  cnntr  23298  cncnp  23303  lmcls  23325  lmcld  23326  iscnrm2  23361  ist0-2  23367  ist1-2  23370  ishaus2  23374  isreg2  23400  ordtt1  23402  sscmp  23428  dfconn2  23442  clsconn  23453  conncompcld  23457  1stccnp  23485  locfincf  23554  kgenval  23558  kgenuni  23562  1stckgenlem  23576  kgen2ss  23578  kgencn2  23580  txtopon  23614  txuni  23615  pttopon  23619  ptuniconst  23621  txcls  23627  ptclsg  23638  dfac14lem  23640  xkoccn  23642  ptcnplem  23644  ptcn  23650  cnmpt1t  23688  cnmpt2t  23696  cnmpt1res  23699  cnmpt2res  23700  cnmptkp  23703  cnmptk1p  23708  cnmptk2  23709  xkoinjcn  23710  elqtop3  23726  qtoptopon  23727  qtopcld  23736  qtoprest  23740  qtopcmap  23742  kqval  23749  kqcldsat  23756  isr0  23760  r0cld  23761  regr1lem  23762  kqnrmlem1  23766  kqnrmlem2  23767  pt1hmeo  23829  xpstopnlem1  23832  neifil  23903  trnei  23915  elflim  23994  flimss2  23995  flimss1  23996  flimopn  23998  fbflim2  24000  flimclslem  24007  flffval  24012  flfnei  24014  cnpflf2  24023  cnflf  24025  cnflf2  24026  isfcls2  24036  fclsopn  24037  fclsnei  24042  fclscmp  24053  ufilcmp  24055  fcfval  24056  fcfnei  24058  fcfelbas  24059  cnpfcf  24064  cnfcf  24065  alexsublem  24067  tmdcn2  24112  tmdgsum  24118  tmdgsum2  24119  symgtgp  24129  subgntr  24130  opnsubg  24131  clssubg  24132  clsnsg  24133  cldsubg  24134  tgpconncompeqg  24135  tgpconncomp  24136  ghmcnp  24138  snclseqg  24139  tgphaus  24140  tgpt1  24141  prdstmdd  24147  prdstgpd  24148  tsmsgsum  24162  tsmsid  24163  tsmsmhm  24169  tsmsadd  24170  tgptsmscld  24174  utop3cls  24275  mopnuni  24466  isxms2  24473  prdsxmslem2  24557  metdseq0  24889  cnmpopc  24968  ishtpy  25017  om1val  25076  pi1val  25083  csscld  25296  clsocv  25297  cfilfcls  25321  relcmpcmet  25365  limcres  25935  limccnp  25940  limccnp2  25941  dvbss  25950  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvcnp2OLD  25970  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmulf  25996  dvmptres2  26014  dvmptcmul  26016  dvmptntr  26023  dvcnvrelem2  26071  ftc1cn  26098  taylthlem1  26429  ulmdvlem3  26459  efrlim  27026  efrlimOLD  27027  zart0  33839  zarmxt1  33840  pl1cn  33915  cvxpconn  35226  cvxsconn  35227  ivthALT  36317  neibastop2  36343  neibastop3  36344  topmeet  36346  topjoin  36347  refsum2cnlem1  44974  dvresntr  45873  rrxunitopnfi  46247