Theorem toponuni 22961

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  ∪ cuni 4862  ‘cfv 6515  Topctop 22940  TopOnctopon 22957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6471  df-fun 6517  df-fv 6523  df-topon 22958

This theorem is referenced by:  toponunii  22963  toponmax  22973  toponss  22974  toponcom  22975  topgele  22977  topontopn  22987  toponmre  23140  cldmreon  23141  restuni  23209  resttopon2  23215  restlp  23230  restperf  23231  perfopn  23232  ordtcld1  23244  ordtcld2  23245  lmfval  23279  cnfval  23280  cnpfval  23281  cnpf2  23297  cnprcl2  23298  ssidcn  23302  iscnp4  23310  iscncl  23316  cncls2  23320  cncls  23321  cnntr  23322  cncnp  23327  lmcls  23349  lmcld  23350  iscnrm2  23385  ist0-2  23391  ist1-2  23394  ishaus2  23398  isreg2  23424  ordtt1  23426  sscmp  23452  dfconn2  23466  clsconn  23477  conncompcld  23481  1stccnp  23509  locfincf  23578  kgenval  23582  kgenuni  23586  1stckgenlem  23600  kgen2ss  23602  kgencn2  23604  txtopon  23638  txuni  23639  pttopon  23643  ptuniconst  23645  txcls  23651  ptclsg  23662  dfac14lem  23664  xkoccn  23666  ptcnplem  23668  ptcn  23674  cnmpt1t  23712  cnmpt2t  23720  cnmpt1res  23723  cnmpt2res  23724  cnmptkp  23727  cnmptk1p  23732  cnmptk2  23733  xkoinjcn  23734  elqtop3  23750  qtoptopon  23751  qtopcld  23760  qtoprest  23764  qtopcmap  23766  kqval  23773  kqcldsat  23780  isr0  23784  r0cld  23785  regr1lem  23786  kqnrmlem1  23790  kqnrmlem2  23791  pt1hmeo  23853  xpstopnlem1  23856  neifil  23927  trnei  23939  elflim  24018  flimss2  24019  flimss1  24020  flimopn  24022  fbflim2  24024  flimclslem  24031  flffval  24036  flfnei  24038  cnpflf2  24047  cnflf  24049  cnflf2  24050  isfcls2  24060  fclsopn  24061  fclsnei  24066  fclscmp  24077  ufilcmp  24079  fcfval  24080  fcfnei  24082  fcfelbas  24083  cnpfcf  24088  cnfcf  24089  alexsublem  24091  tmdcn2  24136  tmdgsum  24142  tmdgsum2  24143  symgtgp  24153  subgntr  24154  opnsubg  24155  clssubg  24156  clsnsg  24157  cldsubg  24158  tgpconncompeqg  24159  tgpconncomp  24160  ghmcnp  24162  snclseqg  24163  tgphaus  24164  tgpt1  24165  prdstmdd  24171  prdstgpd  24172  tsmsgsum  24186  tsmsid  24187  tsmsmhm  24193  tsmsadd  24194  tgptsmscld  24198  utop3cls  24298  mopnuni  24488  isxms2  24495  prdsxmslem2  24576  metdseq0  24902  cnmpopc  24977  ishtpy  25021  om1val  25079  pi1val  25086  csscld  25298  clsocv  25299  cfilfcls  25323  relcmpcmet  25367  limcres  25935  limccnp  25940  limccnp2  25941  dvbss  25950  perfdvf  25952  dvreslem  25958  dvres2lem  25959  dvcnp2  25969  dvaddbr  25987  dvmulbr  25988  dvcmulf  25994  dvmptres2  26011  dvmptcmul  26013  dvmptntr  26020  dvcnvrelem2  26067  ftc1cn  26092  taylthlem1  26423  ulmdvlem3  26452  efrlim  27021  zart0  34136  zarmxt1  34137  pl1cn  34212  cvxpconn  35552  cvxsconn  35553  ivthALT  36655  neibastop2  36681  neibastop3  36682  topmeet  36684  topjoin  36685  refsum2cnlem1  45577  dvresntr  46452  rrxunitopnfi  46826