Theorem sumex 15720

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

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1536  ∃wex 1775   ∈ wcel 2105  ∃wrex 3067  Vcvv 3477  ⦋csb 3907   ⊆ wss 3962  ifcif 4530   class class class wbr 5147   ↦ cmpt 5230  ℩cio 6513  –1-1-onto→wf1o 6561  ‘cfv 6562  (class class class)co 7430  0cc0 11152  1c1 11153   + caddc 11155  ℕcn 12263  ℤcz 12610  ℤ_≥cuz 12875  ...cfz 13543  seqcseq 14038   ⇝ cli 15516  Σcsu 15718

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-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-sn 4631  df-pr 4633  df-uni 4912  df-iota 6515  df-sum 15719

This theorem is referenced by:  fsumrlim  15843  fsumo1  15844  efval  16111  efcvgfsum  16118  eftlub  16141  bitsinv2  16476  bitsinv  16481  lebnumlem3  25008  isi1f  25722  itg1val  25731  itg1climres  25763  itgex  25819  itgfsum  25876  dvmptfsum  26027  plyeq0lem  26263  plyaddlem1  26266  plymullem1  26267  coeeulem  26277  coeid2  26292  plyco  26294  coemullem  26303  coemul  26305  aareccl  26382  aaliou3lem5  26403  aaliou3lem6  26404  aaliou3lem7  26405  taylpval  26422  psercn  26484  pserdvlem2  26486  pserdv  26487  abelthlem6  26494  abelthlem8  26497  abelthlem9  26498  logtayl  26716  leibpi  26999  basellem3  27140  chtval  27167  chpval  27179  sgmval  27199  muinv  27250  dchrvmasumlem1  27553  dchrisum0fval  27563  dchrisum0fno1  27569  dchrisum0lem3  27577  dchrisum0  27578  mulogsum  27590  logsqvma2  27601  selberglem1  27603  pntsval  27630  ecgrtg  29012  esumpcvgval  34058  esumcvg  34066  eulerpartlemsv1  34337  signsplypnf  34543  signsvvfval  34571  vtsval  34630  circlemeth  34633  fwddifnval  36144  knoppndvlem6  36499  binomcxplemnotnn0  44351  stoweidlem11  45966  stoweidlem26  45981  fourierdlem112  46173  fsumlesge0  46332  sge0sn  46334  sge0f1o  46337  sge0supre  46344  sge0resplit  46361  sge0reuz  46402  sge0reuzb  46403  aacllem  49031