Theorem sumex 15599

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 15598	. 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 2829	1 ⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃wrex 3057  Vcvv 3437  ⦋csb 3846   ⊆ wss 3898  ifcif 4476   class class class wbr 5095   ↦ cmpt 5176  ℩cio 6442  –1-1-onto→wf1o 6487  ‘cfv 6488  (class class class)co 7354  0cc0 11015  1c1 11016   + caddc 11018  ℕcn 12134  ℤcz 12477  ℤ_≥cuz 12740  ...cfz 13411  seqcseq 13912   ⇝ cli 15395  Σcsu 15597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-sn 4578  df-pr 4580  df-uni 4861  df-iota 6444  df-sum 15598

This theorem is referenced by:  fsumrlim  15722  fsumo1  15723  efval  15990  efcvgfsum  15997  eftlub  16022  bitsinv2  16358  bitsinv  16363  lebnumlem3  24892  isi1f  25605  itg1val  25614  itg1climres  25645  itgex  25701  itgfsum  25758  dvmptfsum  25909  plyeq0lem  26145  plyaddlem1  26148  plymullem1  26149  coeeulem  26159  coeid2  26174  plyco  26176  coemullem  26185  coemul  26187  aareccl  26264  aaliou3lem5  26285  aaliou3lem6  26286  aaliou3lem7  26287  taylpval  26304  psercn  26366  pserdvlem2  26368  pserdv  26369  abelthlem6  26376  abelthlem8  26379  abelthlem9  26380  logtayl  26599  leibpi  26882  basellem3  27023  chtval  27050  chpval  27062  sgmval  27082  muinv  27133  dchrvmasumlem1  27436  dchrisum0fval  27446  dchrisum0fno1  27452  dchrisum0lem3  27460  dchrisum0  27461  mulogsum  27473  logsqvma2  27484  selberglem1  27486  pntsval  27513  ecgrtg  28965  esumpcvgval  34114  esumcvg  34122  eulerpartlemsv1  34392  signsplypnf  34586  signsvvfval  34614  vtsval  34673  circlemeth  34676  fwddifnval  36230  knoppndvlem6  36584  binomcxplemnotnn0  44476  stoweidlem11  46136  stoweidlem26  46151  fourierdlem112  46343  fsumlesge0  46502  sge0sn  46504  sge0f1o  46507  sge0supre  46514  sge0resplit  46531  sge0reuz  46572  sge0reuzb  46573  aacllem  49929