Theorem sumex 15648

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

Syntax hints:   ∧ wa 396   ∨ wo 853   = wceq 1547  ∃wex 1786   ∈ wcel 2119  ∃wrex 3064  Vcvv 3432  ⦋csb 3838   ⊆ wss 3890  ifcif 4461   class class class wbr 5079   ↦ cmpt 5160  ℩cio 6446  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7363  0cc0 11036  1c1 11037   + caddc 11039  ℕcn 12172  ℤcz 12522  ℤ_≥cuz 12786  ...cfz 13459  seqcseq 13961   ⇝ cli 15444  Σcsu 15646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-sn 4563  df-pr 4565  df-uni 4846  df-iota 6448  df-sum 15647

This theorem is referenced by:  fsumrlim  15772  fsumo1  15773  efval  16042  efcvgfsum  16049  eftlub  16074  bitsinv2  16410  bitsinv  16415  lebnumlem3  24955  isi1f  25666  itg1val  25675  itg1climres  25706  itgex  25762  itgfsum  25819  dvmptfsum  25967  plyeq0lem  26200  plyaddlem1  26203  plymullem1  26204  coeeulem  26214  coeid2  26229  plyco  26231  coemullem  26240  coemul  26242  aareccl  26317  aaliou3lem5  26338  aaliou3lem6  26339  aaliou3lem7  26340  taylpval  26357  psercn  26416  pserdvlem2  26418  pserdv  26419  abelthlem6  26426  abelthlem8  26429  abelthlem9  26430  logtayl  26649  leibpi  26931  basellem3  27071  chtval  27098  chpval  27110  sgmval  27130  muinv  27181  dchrvmasumlem1  27483  dchrisum0fval  27493  dchrisum0fno1  27499  dchrisum0lem3  27507  dchrisum0  27508  mulogsum  27520  logsqvma2  27531  selberglem1  27533  pntsval  27560  ecgrtg  29077  esumpcvgval  34269  esumcvg  34277  eulerpartlemsv1  34547  signsplypnf  34741  signsvvfval  34769  vtsval  34828  circlemeth  34831  fwddifnval  36398  knoppndvlem6  36830  binomcxplemnotnn0  44807  stoweidlem11  46461  stoweidlem26  46476  fourierdlem112  46668  fsumlesge0  46827  sge0sn  46829  sge0f1o  46832  sge0supre  46839  sge0resplit  46856  sge0reuz  46897  sge0reuzb  46898  aacllem  50298