Theorem sumex 15848

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

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2145  ∃wrex 3087  Vcvv 3451  ⦋csb 3847   ⊆ wss 3899  ifcif 4482   class class class wbr 5103   ↦ cmpt 5186  ℩cio 6491  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7418  0cc0 11193  1c1 11194   + caddc 11196  ℕcn 12328  ℤcz 12686  ℤ_≥cuz 12958  ...cfz 13632  seqcseq 14137   ⇝ cli 15644  Σcsu 15846

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6493  df-sum 15847

This theorem is used by:  fsumrlim  15971  fsumo1  15972  efval  16238  efcvgfsum  16245  eftlub  16270  bitsinv2  16606  bitsinv  16611  lebnumlem3  25277  isi1f  25988  itg1val  25997  itg1climres  26028  itgex  26084  itgfsum  26140  dvmptfsum  26288  plyeq0lem  26522  plyaddlem1  26525  plymullem1  26526  coeeulem  26536  coeid2  26551  plyco  26553  coemullem  26562  coemul  26564  aareccl  26646  aaliou3lem5  26667  aaliou3lem6  26668  aaliou3lem7  26669  taylpval  26687  psercn  26746  pserdvlem2  26748  pserdv  26749  abelthlem6  26756  abelthlem8  26759  abelthlem9  26760  logtayl  26981  leibpi  27263  basellem3  27403  chtval  27430  chpval  27442  sgmval  27462  muinv  27513  dchrvmasumlem1  27815  dchrisum0fval  27825  dchrisum0fno1  27831  dchrisum0lem3  27839  dchrisum0  27840  mulogsum  27852  logsqvma2  27863  selberglem1  27865  pntsval  27892  ecgrtg  29554  esumpcvgval  34703  esumcvg  34711  eulerpartlemsv1  34981  signsplypnf  35172  signsvvfval  35200  vtsval  35259  circlemeth  35262  fwddifnval  36908  knoppndvlem6  37363  binomcxplemnotnn0  45325  stoweidlem11  46990  stoweidlem26  47005  fourierdlem112  47197  fsumlesge0  47356  sge0sn  47358  sge0f1o  47361  sge0supre  47368  sge0resplit  47385  sge0reuz  47426  sge0reuzb  47427  aacllem  50908