Theorem sumex 15724

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

Syntax hints:   ∧ wa 395   ∨ wo 848   = wceq 1540  ∃wex 1779   ∈ wcel 2108  ∃wrex 3070  Vcvv 3480  ⦋csb 3899   ⊆ wss 3951  ifcif 4525   class class class wbr 5143   ↦ cmpt 5225  ℩cio 6512  –1-1-onto→wf1o 6560  ‘cfv 6561  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158  ℕcn 12266  ℤcz 12613  ℤ_≥cuz 12878  ...cfz 13547  seqcseq 14042   ⇝ cli 15520  Σcsu 15722

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-sum 15723

This theorem is referenced by:  fsumrlim  15847  fsumo1  15848  efval  16115  efcvgfsum  16122  eftlub  16145  bitsinv2  16480  bitsinv  16485  lebnumlem3  24995  isi1f  25709  itg1val  25718  itg1climres  25749  itgex  25805  itgfsum  25862  dvmptfsum  26013  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeid2  26278  plyco  26280  coemullem  26289  coemul  26291  aareccl  26368  aaliou3lem5  26389  aaliou3lem6  26390  aaliou3lem7  26391  taylpval  26408  psercn  26470  pserdvlem2  26472  pserdv  26473  abelthlem6  26480  abelthlem8  26483  abelthlem9  26484  logtayl  26702  leibpi  26985  basellem3  27126  chtval  27153  chpval  27165  sgmval  27185  muinv  27236  dchrvmasumlem1  27539  dchrisum0fval  27549  dchrisum0fno1  27555  dchrisum0lem3  27563  dchrisum0  27564  mulogsum  27576  logsqvma2  27587  selberglem1  27589  pntsval  27616  ecgrtg  28998  esumpcvgval  34079  esumcvg  34087  eulerpartlemsv1  34358  signsplypnf  34565  signsvvfval  34593  vtsval  34652  circlemeth  34655  fwddifnval  36164  knoppndvlem6  36518  binomcxplemnotnn0  44375  stoweidlem11  46026  stoweidlem26  46041  fourierdlem112  46233  fsumlesge0  46392  sge0sn  46394  sge0f1o  46397  sge0supre  46404  sge0resplit  46421  sge0reuz  46462  sge0reuzb  46463  aacllem  49320