Theorem sumex 15736

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

Syntax hints:   ∧ wa 395   ∨ wo 846   = wceq 1537  ∃wex 1777   ∈ wcel 2108  ∃wrex 3076  Vcvv 3488  ⦋csb 3921   ⊆ wss 3976  ifcif 4548   class class class wbr 5166   ↦ cmpt 5249  ℩cio 6523  –1-1-onto→wf1o 6572  ‘cfv 6573  (class class class)co 7448  0cc0 11184  1c1 11185   + caddc 11187  ℕcn 12293  ℤcz 12639  ℤ_≥cuz 12903  ...cfz 13567  seqcseq 14052   ⇝ cli 15530  Σcsu 15734

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-sum 15735

This theorem is referenced by:  fsumrlim  15859  fsumo1  15860  efval  16127  efcvgfsum  16134  eftlub  16157  bitsinv2  16489  bitsinv  16494  lebnumlem3  25014  isi1f  25728  itg1val  25737  itg1climres  25769  itgex  25825  itgfsum  25882  dvmptfsum  26033  plyeq0lem  26269  plyaddlem1  26272  plymullem1  26273  coeeulem  26283  coeid2  26298  plyco  26300  coemullem  26309  coemul  26311  aareccl  26386  aaliou3lem5  26407  aaliou3lem6  26408  aaliou3lem7  26409  taylpval  26426  psercn  26488  pserdvlem2  26490  pserdv  26491  abelthlem6  26498  abelthlem8  26501  abelthlem9  26502  logtayl  26720  leibpi  27003  basellem3  27144  chtval  27171  chpval  27183  sgmval  27203  muinv  27254  dchrvmasumlem1  27557  dchrisum0fval  27567  dchrisum0fno1  27573  dchrisum0lem3  27581  dchrisum0  27582  mulogsum  27594  logsqvma2  27605  selberglem1  27607  pntsval  27634  ecgrtg  29016  esumpcvgval  34042  esumcvg  34050  eulerpartlemsv1  34321  signsplypnf  34527  signsvvfval  34555  vtsval  34614  circlemeth  34617  fwddifnval  36127  knoppndvlem6  36483  binomcxplemnotnn0  44325  stoweidlem11  45932  stoweidlem26  45947  fourierdlem112  46139  fsumlesge0  46298  sge0sn  46300  sge0f1o  46303  sge0supre  46310  sge0resplit  46327  sge0reuz  46368  sge0reuzb  46369  aacllem  48895