Theorem sumex 15623

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

Syntax hints:   ∧ wa 395   ∨ wo 848   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3062  Vcvv 3442  ⦋csb 3851   ⊆ wss 3903  ifcif 4481   class class class wbr 5100   ↦ cmpt 5181  ℩cio 6454  –1-1-onto→wf1o 6499  ‘cfv 6500  (class class class)co 7368  0cc0 11038  1c1 11039   + caddc 11041  ℕcn 12157  ℤcz 12500  ℤ_≥cuz 12763  ...cfz 13435  seqcseq 13936   ⇝ cli 15419  Σcsu 15621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6456  df-sum 15622

This theorem is referenced by:  fsumrlim  15746  fsumo1  15747  efval  16014  efcvgfsum  16021  eftlub  16046  bitsinv2  16382  bitsinv  16387  lebnumlem3  24930  isi1f  25643  itg1val  25652  itg1climres  25683  itgex  25739  itgfsum  25796  dvmptfsum  25947  plyeq0lem  26183  plyaddlem1  26186  plymullem1  26187  coeeulem  26197  coeid2  26212  plyco  26214  coemullem  26223  coemul  26225  aareccl  26302  aaliou3lem5  26323  aaliou3lem6  26324  aaliou3lem7  26325  taylpval  26342  psercn  26404  pserdvlem2  26406  pserdv  26407  abelthlem6  26414  abelthlem8  26417  abelthlem9  26418  logtayl  26637  leibpi  26920  basellem3  27061  chtval  27088  chpval  27100  sgmval  27120  muinv  27171  dchrvmasumlem1  27474  dchrisum0fval  27484  dchrisum0fno1  27490  dchrisum0lem3  27498  dchrisum0  27499  mulogsum  27511  logsqvma2  27522  selberglem1  27524  pntsval  27551  ecgrtg  29068  esumpcvgval  34255  esumcvg  34263  eulerpartlemsv1  34533  signsplypnf  34727  signsvvfval  34755  vtsval  34814  circlemeth  34817  fwddifnval  36376  knoppndvlem6  36736  binomcxplemnotnn0  44709  stoweidlem11  46366  stoweidlem26  46381  fourierdlem112  46573  fsumlesge0  46732  sge0sn  46734  sge0f1o  46737  sge0supre  46744  sge0resplit  46761  sge0reuz  46802  sge0reuzb  46803  aacllem  50157