Theorem sumex 15641

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

Syntax hints:   ∧ wa 395   ∨ wo 844   = wceq 1540  ∃wex 1780   ∈ wcel 2105  ∃wrex 3069  Vcvv 3473  ⦋csb 3893   ⊆ wss 3948  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  ℩cio 6493  –1-1-onto→wf1o 6542  ‘cfv 6543  (class class class)co 7412  0cc0 11116  1c1 11117   + caddc 11119  ℕcn 12219  ℤcz 12565  ℤ_≥cuz 12829  ...cfz 13491  seqcseq 13973   ⇝ cli 15435  Σcsu 15639

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-sn 4629  df-pr 4631  df-uni 4909  df-iota 6495  df-sum 15640

This theorem is referenced by:  fsumrlim  15764  fsumo1  15765  efval  16030  efcvgfsum  16036  eftlub  16059  bitsinv2  16391  bitsinv  16396  lebnumlem3  24809  isi1f  25523  itg1val  25532  itg1climres  25564  itgex  25620  itgfsum  25676  dvmptfsum  25827  plyeq0lem  26062  plyaddlem1  26065  plymullem1  26066  coeeulem  26076  coeid2  26091  plyco  26093  coemullem  26102  coemul  26104  aareccl  26178  aaliou3lem5  26199  aaliou3lem6  26200  aaliou3lem7  26201  taylpval  26218  psercn  26278  pserdvlem2  26280  pserdv  26281  abelthlem6  26288  abelthlem8  26291  abelthlem9  26292  logtayl  26508  leibpi  26788  basellem3  26928  chtval  26955  chpval  26967  sgmval  26987  muinv  27038  dchrvmasumlem1  27341  dchrisum0fval  27351  dchrisum0fno1  27357  dchrisum0lem3  27365  dchrisum0  27366  mulogsum  27378  logsqvma2  27389  selberglem1  27391  pntsval  27418  ecgrtg  28674  esumpcvgval  33540  esumcvg  33548  eulerpartlemsv1  33819  signsplypnf  34025  signsvvfval  34053  vtsval  34113  circlemeth  34116  fwddifnval  35605  knoppndvlem6  35857  binomcxplemnotnn0  43578  stoweidlem11  45186  stoweidlem26  45201  fourierdlem112  45393  fsumlesge0  45552  sge0sn  45554  sge0f1o  45557  sge0supre  45564  sge0resplit  45581  sge0reuz  45622  sge0reuzb  45623  aacllem  48010