Theorem sumex 15661

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

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1540  ∃wex 1779   ∈ wcel 2109  ∃wrex 3054  Vcvv 3450  ⦋csb 3865   ⊆ wss 3917  ifcif 4491   class class class wbr 5110   ↦ cmpt 5191  ℩cio 6465  –1-1-onto→wf1o 6513  ‘cfv 6514  (class class class)co 7390  0cc0 11075  1c1 11076   + caddc 11078  ℕcn 12193  ℤcz 12536  ℤ_≥cuz 12800  ...cfz 13475  seqcseq 13973   ⇝ cli 15457  Σcsu 15659

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 2702  ax-nul 5264

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 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6467  df-sum 15660

This theorem is referenced by:  fsumrlim  15784  fsumo1  15785  efval  16052  efcvgfsum  16059  eftlub  16084  bitsinv2  16420  bitsinv  16425  lebnumlem3  24869  isi1f  25582  itg1val  25591  itg1climres  25622  itgex  25678  itgfsum  25735  dvmptfsum  25886  plyeq0lem  26122  plyaddlem1  26125  plymullem1  26126  coeeulem  26136  coeid2  26151  plyco  26153  coemullem  26162  coemul  26164  aareccl  26241  aaliou3lem5  26262  aaliou3lem6  26263  aaliou3lem7  26264  taylpval  26281  psercn  26343  pserdvlem2  26345  pserdv  26346  abelthlem6  26353  abelthlem8  26356  abelthlem9  26357  logtayl  26576  leibpi  26859  basellem3  27000  chtval  27027  chpval  27039  sgmval  27059  muinv  27110  dchrvmasumlem1  27413  dchrisum0fval  27423  dchrisum0fno1  27429  dchrisum0lem3  27437  dchrisum0  27438  mulogsum  27450  logsqvma2  27461  selberglem1  27463  pntsval  27490  ecgrtg  28917  esumpcvgval  34075  esumcvg  34083  eulerpartlemsv1  34354  signsplypnf  34548  signsvvfval  34576  vtsval  34635  circlemeth  34638  fwddifnval  36158  knoppndvlem6  36512  binomcxplemnotnn0  44352  stoweidlem11  46016  stoweidlem26  46031  fourierdlem112  46223  fsumlesge0  46382  sge0sn  46384  sge0f1o  46387  sge0supre  46394  sge0resplit  46411  sge0reuz  46452  sge0reuzb  46453  aacllem  49794