Theorem sumex 15595

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

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∃wrex 3056  Vcvv 3436  ⦋csb 3850   ⊆ wss 3902  ifcif 4475   class class class wbr 5091   ↦ cmpt 5172  ℩cio 6435  –1-1-onto→wf1o 6480  ‘cfv 6481  (class class class)co 7346  0cc0 11006  1c1 11007   + caddc 11009  ℕcn 12125  ℤcz 12468  ℤ_≥cuz 12732  ...cfz 13407  seqcseq 13908   ⇝ cli 15391  Σcsu 15593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4577  df-pr 4579  df-uni 4860  df-iota 6437  df-sum 15594

This theorem is referenced by:  fsumrlim  15718  fsumo1  15719  efval  15986  efcvgfsum  15993  eftlub  16018  bitsinv2  16354  bitsinv  16359  lebnumlem3  24890  isi1f  25603  itg1val  25612  itg1climres  25643  itgex  25699  itgfsum  25756  dvmptfsum  25907  plyeq0lem  26143  plyaddlem1  26146  plymullem1  26147  coeeulem  26157  coeid2  26172  plyco  26174  coemullem  26183  coemul  26185  aareccl  26262  aaliou3lem5  26283  aaliou3lem6  26284  aaliou3lem7  26285  taylpval  26302  psercn  26364  pserdvlem2  26366  pserdv  26367  abelthlem6  26374  abelthlem8  26377  abelthlem9  26378  logtayl  26597  leibpi  26880  basellem3  27021  chtval  27048  chpval  27060  sgmval  27080  muinv  27131  dchrvmasumlem1  27434  dchrisum0fval  27444  dchrisum0fno1  27450  dchrisum0lem3  27458  dchrisum0  27459  mulogsum  27471  logsqvma2  27482  selberglem1  27484  pntsval  27511  ecgrtg  28962  esumpcvgval  34089  esumcvg  34097  eulerpartlemsv1  34367  signsplypnf  34561  signsvvfval  34589  vtsval  34648  circlemeth  34651  fwddifnval  36203  knoppndvlem6  36557  binomcxplemnotnn0  44395  stoweidlem11  46055  stoweidlem26  46070  fourierdlem112  46262  fsumlesge0  46421  sge0sn  46423  sge0f1o  46426  sge0supre  46433  sge0resplit  46450  sge0reuz  46491  sge0reuzb  46492  aacllem  49839