Theorem sumex 15613

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

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3053  Vcvv 3438  ⦋csb 3853   ⊆ wss 3905  ifcif 4478   class class class wbr 5095   ↦ cmpt 5176  ℩cio 6440  –1-1-onto→wf1o 6485  ‘cfv 6486  (class class class)co 7353  0cc0 11028  1c1 11029   + caddc 11031  ℕcn 12146  ℤcz 12489  ℤ_≥cuz 12753  ...cfz 13428  seqcseq 13926   ⇝ cli 15409  Σcsu 15611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862  df-iota 6442  df-sum 15612

This theorem is referenced by:  fsumrlim  15736  fsumo1  15737  efval  16004  efcvgfsum  16011  eftlub  16036  bitsinv2  16372  bitsinv  16377  lebnumlem3  24878  isi1f  25591  itg1val  25600  itg1climres  25631  itgex  25687  itgfsum  25744  dvmptfsum  25895  plyeq0lem  26131  plyaddlem1  26134  plymullem1  26135  coeeulem  26145  coeid2  26160  plyco  26162  coemullem  26171  coemul  26173  aareccl  26250  aaliou3lem5  26271  aaliou3lem6  26272  aaliou3lem7  26273  taylpval  26290  psercn  26352  pserdvlem2  26354  pserdv  26355  abelthlem6  26362  abelthlem8  26365  abelthlem9  26366  logtayl  26585  leibpi  26868  basellem3  27009  chtval  27036  chpval  27048  sgmval  27068  muinv  27119  dchrvmasumlem1  27422  dchrisum0fval  27432  dchrisum0fno1  27438  dchrisum0lem3  27446  dchrisum0  27447  mulogsum  27459  logsqvma2  27470  selberglem1  27472  pntsval  27499  ecgrtg  28946  esumpcvgval  34047  esumcvg  34055  eulerpartlemsv1  34326  signsplypnf  34520  signsvvfval  34548  vtsval  34607  circlemeth  34610  fwddifnval  36139  knoppndvlem6  36493  binomcxplemnotnn0  44332  stoweidlem11  45996  stoweidlem26  46011  fourierdlem112  46203  fsumlesge0  46362  sge0sn  46364  sge0f1o  46367  sge0supre  46374  sge0resplit  46391  sge0reuz  46432  sge0reuzb  46433  aacllem  49790