Theorem sumex 15634

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

Syntax hints:   ∧ wa 397   ∨ wo 846   = wceq 1542  ∃wex 1782   ∈ wcel 2107  ∃wrex 3071  Vcvv 3475  ⦋csb 3894   ⊆ wss 3949  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  ℩cio 6494  –1-1-onto→wf1o 6543  ‘cfv 6544  (class class class)co 7409  0cc0 11110  1c1 11111   + caddc 11113  ℕcn 12212  ℤcz 12558  ℤ_≥cuz 12822  ...cfz 13484  seqcseq 13966   ⇝ cli 15428  Σcsu 15632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-sum 15633

This theorem is referenced by:  fsumrlim  15757  fsumo1  15758  efval  16023  efcvgfsum  16029  eftlub  16052  bitsinv2  16384  bitsinv  16389  lebnumlem3  24479  isi1f  25191  itg1val  25200  itg1climres  25232  itgex  25288  itgfsum  25344  dvmptfsum  25492  plyeq0lem  25724  plyaddlem1  25727  plymullem1  25728  coeeulem  25738  coeid2  25753  plyco  25755  coemullem  25764  coemul  25766  aareccl  25839  aaliou3lem5  25860  aaliou3lem6  25861  aaliou3lem7  25862  taylpval  25879  psercn  25938  pserdvlem2  25940  pserdv  25941  abelthlem6  25948  abelthlem8  25951  abelthlem9  25952  logtayl  26168  leibpi  26447  basellem3  26587  chtval  26614  chpval  26626  sgmval  26646  muinv  26697  dchrvmasumlem1  26998  dchrisum0fval  27008  dchrisum0fno1  27014  dchrisum0lem3  27022  dchrisum0  27023  mulogsum  27035  logsqvma2  27046  selberglem1  27048  pntsval  27075  ecgrtg  28241  esumpcvgval  33076  esumcvg  33084  eulerpartlemsv1  33355  signsplypnf  33561  signsvvfval  33589  vtsval  33649  circlemeth  33652  fwddifnval  35135  knoppndvlem6  35393  binomcxplemnotnn0  43115  stoweidlem11  44727  stoweidlem26  44742  fourierdlem112  44934  fsumlesge0  45093  sge0sn  45095  sge0f1o  45098  sge0supre  45105  sge0resplit  45122  sge0reuz  45163  sge0reuzb  45164  aacllem  47848