Theorem sumex 15399

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 15398	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		iotaex 6413	. 2 ⊢ (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚)))) ∈ V
3	1, 2	eqeltri 2835	1 ⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∧ wa 396   ∨ wo 844   = wceq 1539  ∃wex 1782   ∈ wcel 2106  ∃wrex 3065  Vcvv 3432  ⦋csb 3832   ⊆ wss 3887  ifcif 4459   class class class wbr 5074   ↦ cmpt 5157  ℩cio 6389  –1-1-onto→wf1o 6432  ‘cfv 6433  (class class class)co 7275  0cc0 10871  1c1 10872   + caddc 10874  ℕcn 11973  ℤcz 12319  ℤ_≥cuz 12582  ...cfz 13239  seqcseq 13721   ⇝ cli 15193  Σcsu 15397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840  df-iota 6391  df-sum 15398

This theorem is referenced by:  fsumrlim  15523  fsumo1  15524  efval  15789  efcvgfsum  15795  eftlub  15818  bitsinv2  16150  bitsinv  16155  lebnumlem3  24126  isi1f  24838  itg1val  24847  itg1climres  24879  itgex  24935  itgfsum  24991  dvmptfsum  25139  plyeq0lem  25371  plyaddlem1  25374  plymullem1  25375  coeeulem  25385  coeid2  25400  plyco  25402  coemullem  25411  coemul  25413  aareccl  25486  aaliou3lem5  25507  aaliou3lem6  25508  aaliou3lem7  25509  taylpval  25526  psercn  25585  pserdvlem2  25587  pserdv  25588  abelthlem6  25595  abelthlem8  25598  abelthlem9  25599  logtayl  25815  leibpi  26092  basellem3  26232  chtval  26259  chpval  26271  sgmval  26291  muinv  26342  dchrvmasumlem1  26643  dchrisum0fval  26653  dchrisum0fno1  26659  dchrisum0lem3  26667  dchrisum0  26668  mulogsum  26680  logsqvma2  26691  selberglem1  26693  pntsval  26720  ecgrtg  27351  esumpcvgval  32046  esumcvg  32054  eulerpartlemsv1  32323  signsplypnf  32529  signsvvfval  32557  vtsval  32617  circlemeth  32620  fwddifnval  34465  knoppndvlem6  34697  binomcxplemnotnn0  41974  stoweidlem11  43552  stoweidlem26  43567  fourierdlem112  43759  fsumlesge0  43915  sge0sn  43917  sge0f1o  43920  sge0supre  43927  sge0resplit  43944  sge0reuz  43985  sge0reuzb  43986  aacllem  46505