Theorem sumex 15654

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 15653	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		iotaex 6484	. 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 3447  ⦋csb 3862   ⊆ wss 3914  ifcif 4488   class class class wbr 5107   ↦ cmpt 5188  ℩cio 6462  –1-1-onto→wf1o 6510  ‘cfv 6511  (class class class)co 7387  0cc0 11068  1c1 11069   + caddc 11071  ℕcn 12186  ℤcz 12529  ℤ_≥cuz 12793  ...cfz 13468  seqcseq 13966   ⇝ cli 15450  Σcsu 15652

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 5261

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 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-sn 4590  df-pr 4592  df-uni 4872  df-iota 6464  df-sum 15653

This theorem is referenced by:  fsumrlim  15777  fsumo1  15778  efval  16045  efcvgfsum  16052  eftlub  16077  bitsinv2  16413  bitsinv  16418  lebnumlem3  24862  isi1f  25575  itg1val  25584  itg1climres  25615  itgex  25671  itgfsum  25728  dvmptfsum  25879  plyeq0lem  26115  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeid2  26144  plyco  26146  coemullem  26155  coemul  26157  aareccl  26234  aaliou3lem5  26255  aaliou3lem6  26256  aaliou3lem7  26257  taylpval  26274  psercn  26336  pserdvlem2  26338  pserdv  26339  abelthlem6  26346  abelthlem8  26349  abelthlem9  26350  logtayl  26569  leibpi  26852  basellem3  26993  chtval  27020  chpval  27032  sgmval  27052  muinv  27103  dchrvmasumlem1  27406  dchrisum0fval  27416  dchrisum0fno1  27422  dchrisum0lem3  27430  dchrisum0  27431  mulogsum  27443  logsqvma2  27454  selberglem1  27456  pntsval  27483  ecgrtg  28910  esumpcvgval  34068  esumcvg  34076  eulerpartlemsv1  34347  signsplypnf  34541  signsvvfval  34569  vtsval  34628  circlemeth  34631  fwddifnval  36151  knoppndvlem6  36505  binomcxplemnotnn0  44345  stoweidlem11  46009  stoweidlem26  46024  fourierdlem112  46216  fsumlesge0  46375  sge0sn  46377  sge0f1o  46380  sge0supre  46387  sge0resplit  46404  sge0reuz  46445  sge0reuzb  46446  aacllem  49790