Theorem sumex 15758

Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Assertion

Ref	Expression
sumex	⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V

Proof of Theorem sumex

Dummy variables 𝑓 𝑚 𝑛 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sum 15757	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		iotaex 6516	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) ∈ V
3	1, 2	eqeltri 2861	1 ⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2146  ∃wrex 3091  Vcvv 3457  ⦋csb 3854   ⊆ wss 3906  ifcif 4489   class class class wbr 5111   ↦ cmpt 5194  ℩cio 6494  –1-1-onto→wf1o 6539  ‘cfv 6540  (class class class)co 7416  0cc0 11111  1c1 11112   + caddc 11114  ℕcn 12244  ℤcz 12602  ℤ_≥cuz 12873  ...cfz 13546  seqcseq 14050   ⇝ cli 15554  Σcsu 15756

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-sn 4592  df-pr 4594  df-uni 4875  df-iota 6496  df-sum 15757

This theorem is used by:  fsumrlim  15881  fsumo1  15882  efval  16150  efcvgfsum  16157  eftlub  16182  bitsinv2  16518  bitsinv  16523  lebnumlem3  25151  isi1f  25862  itg1val  25871  itg1climres  25902  itgex  25958  itgfsum  26015  dvmptfsum  26163  plyeq0lem  26396  plyaddlem1  26399  plymullem1  26400  coeeulem  26410  coeid2  26425  plyco  26427  coemullem  26436  coemul  26438  aareccl  26518  aaliou3lem5  26539  aaliou3lem6  26540  aaliou3lem7  26541  taylpval  26559  psercn  26618  pserdvlem2  26620  pserdv  26621  abelthlem6  26628  abelthlem8  26631  abelthlem9  26632  logtayl  26854  leibpi  27136  basellem3  27276  chtval  27303  chpval  27315  sgmval  27335  muinv  27386  dchrvmasumlem1  27688  dchrisum0fval  27698  dchrisum0fno1  27704  dchrisum0lem3  27712  dchrisum0  27713  mulogsum  27725  logsqvma2  27736  selberglem1  27738  pntsval  27765  ecgrtg  29362  esumpcvgval  34491  esumcvg  34499  eulerpartlemsv1  34770  signsplypnf  34961  signsvvfval  34989  vtsval  35048  circlemeth  35051  fwddifnval  36668  knoppndvlem6  37139  binomcxplemnotnn0  45099  stoweidlem11  46758  stoweidlem26  46773  fourierdlem112  46965  fsumlesge0  47124  sge0sn  47126  sge0f1o  47129  sge0supre  47136  sge0resplit  47153  sge0reuz  47194  sge0reuzb  47195  aacllem  50654