Theorem sumex 15645

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

Syntax hints:   ∧ wa 397   ∨ wo 854   = wceq 1548  ∃wex 1787   ∈ wcel 2121  ∃wrex 3065  Vcvv 3433  ⦋csb 3832   ⊆ wss 3884  ifcif 4456   class class class wbr 5074   ↦ cmpt 5155  ℩cio 6442  –1-1-onto→wf1o 6487  ‘cfv 6488  (class class class)co 7359  0cc0 11034  1c1 11035   + caddc 11037  ℕcn 12169  ℤcz 12519  ℤ_≥cuz 12783  ...cfz 13456  seqcseq 13958   ⇝ cli 15441  Σcsu 15643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713  ax-nul 5230

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-fal 1561  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-v 3435  df-dif 3887  df-un 3889  df-ss 3901  df-nul 4264  df-sn 4558  df-pr 4560  df-uni 4841  df-iota 6444  df-sum 15644

This theorem is referenced by:  fsumrlim  15769  fsumo1  15770  efval  16039  efcvgfsum  16046  eftlub  16071  bitsinv2  16407  bitsinv  16412  lebnumlem3  24951  isi1f  25662  itg1val  25671  itg1climres  25702  itgex  25758  itgfsum  25815  dvmptfsum  25963  plyeq0lem  26196  plyaddlem1  26199  plymullem1  26200  coeeulem  26210  coeid2  26225  plyco  26227  coemullem  26236  coemul  26238  aareccl  26313  aaliou3lem5  26334  aaliou3lem6  26335  aaliou3lem7  26336  taylpval  26353  psercn  26412  pserdvlem2  26414  pserdv  26415  abelthlem6  26422  abelthlem8  26425  abelthlem9  26426  logtayl  26645  leibpi  26927  basellem3  27067  chtval  27094  chpval  27106  sgmval  27126  muinv  27177  dchrvmasumlem1  27479  dchrisum0fval  27489  dchrisum0fno1  27495  dchrisum0lem3  27503  dchrisum0  27504  mulogsum  27516  logsqvma2  27527  selberglem1  27529  pntsval  27556  ecgrtg  29072  esumpcvgval  34272  esumcvg  34280  eulerpartlemsv1  34550  signsplypnf  34744  signsvvfval  34772  vtsval  34831  circlemeth  34834  fwddifnval  36404  knoppndvlem6  36836  binomcxplemnotnn0  44813  stoweidlem11  46466  stoweidlem26  46481  fourierdlem112  46673  fsumlesge0  46832  sge0sn  46834  sge0f1o  46837  sge0supre  46844  sge0resplit  46861  sge0reuz  46902  sge0reuzb  46903  aacllem  50303