Theorem sumex 15044

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

Syntax hints:   ∧ wa 398   ∨ wo 843   = wceq 1537  ∃wex 1780   ∈ wcel 2114  ∃wrex 3139  Vcvv 3494  ⦋csb 3883   ⊆ wss 3936  ifcif 4467   class class class wbr 5066   ↦ cmpt 5146  ℩cio 6312  –1-1-onto→wf1o 6354  ‘cfv 6355  (class class class)co 7156  0cc0 10537  1c1 10538   + caddc 10540  ℕcn 11638  ℤcz 11982  ℤ_≥cuz 12244  ...cfz 12893  seqcseq 13370   ⇝ cli 14841  Σcsu 15042

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-sn 4568  df-pr 4570  df-uni 4839  df-iota 6314  df-sum 15043

This theorem is referenced by:  fsumrlim  15166  fsumo1  15167  efval  15433  efcvgfsum  15439  eftlub  15462  bitsinv2  15792  bitsinv  15797  lebnumlem3  23567  isi1f  24275  itg1val  24284  itg1climres  24315  itgex  24371  itgfsum  24427  dvmptfsum  24572  plyeq0lem  24800  plyaddlem1  24803  plymullem1  24804  coeeulem  24814  coeid2  24829  plyco  24831  coemullem  24840  coemul  24842  aareccl  24915  aaliou3lem5  24936  aaliou3lem6  24937  aaliou3lem7  24938  taylpval  24955  psercn  25014  pserdvlem2  25016  pserdv  25017  abelthlem6  25024  abelthlem8  25027  abelthlem9  25028  logtayl  25243  leibpi  25520  basellem3  25660  chtval  25687  chpval  25699  sgmval  25719  muinv  25770  dchrvmasumlem1  26071  dchrisum0fval  26081  dchrisum0fno1  26087  dchrisum0lem3  26095  dchrisum0  26096  mulogsum  26108  logsqvma2  26119  selberglem1  26121  pntsval  26148  ecgrtg  26769  esumpcvgval  31337  esumcvg  31345  eulerpartlemsv1  31614  signsplypnf  31820  signsvvfval  31848  vtsval  31908  circlemeth  31911  fwddifnval  33624  knoppndvlem6  33856  binomcxplemnotnn0  40708  stoweidlem11  42316  stoweidlem26  42331  fourierdlem112  42523  fsumlesge0  42679  sge0sn  42681  sge0f1o  42684  sge0supre  42691  sge0resplit  42708  sge0reuz  42749  sge0reuzb  42750  aacllem  44922