Theorem sumex 15611

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

Syntax hints:   ∧ wa 395   ∨ wo 847   = wceq 1541  ∃wex 1780   ∈ wcel 2113  ∃wrex 3060  Vcvv 3440  ⦋csb 3849   ⊆ wss 3901  ifcif 4479   class class class wbr 5098   ↦ cmpt 5179  ℩cio 6446  –1-1-onto→wf1o 6491  ‘cfv 6492  (class class class)co 7358  0cc0 11026  1c1 11027   + caddc 11029  ℕcn 12145  ℤcz 12488  ℤ_≥cuz 12751  ...cfz 13423  seqcseq 13924   ⇝ cli 15407  Σcsu 15609

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 2708  ax-nul 5251

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448  df-sum 15610

This theorem is referenced by:  fsumrlim  15734  fsumo1  15735  efval  16002  efcvgfsum  16009  eftlub  16034  bitsinv2  16370  bitsinv  16375  lebnumlem3  24918  isi1f  25631  itg1val  25640  itg1climres  25671  itgex  25727  itgfsum  25784  dvmptfsum  25935  plyeq0lem  26171  plyaddlem1  26174  plymullem1  26175  coeeulem  26185  coeid2  26200  plyco  26202  coemullem  26211  coemul  26213  aareccl  26290  aaliou3lem5  26311  aaliou3lem6  26312  aaliou3lem7  26313  taylpval  26330  psercn  26392  pserdvlem2  26394  pserdv  26395  abelthlem6  26402  abelthlem8  26405  abelthlem9  26406  logtayl  26625  leibpi  26908  basellem3  27049  chtval  27076  chpval  27088  sgmval  27108  muinv  27159  dchrvmasumlem1  27462  dchrisum0fval  27472  dchrisum0fno1  27478  dchrisum0lem3  27486  dchrisum0  27487  mulogsum  27499  logsqvma2  27510  selberglem1  27512  pntsval  27539  ecgrtg  29056  esumpcvgval  34235  esumcvg  34243  eulerpartlemsv1  34513  signsplypnf  34707  signsvvfval  34735  vtsval  34794  circlemeth  34797  fwddifnval  36357  knoppndvlem6  36717  binomcxplemnotnn0  44597  stoweidlem11  46255  stoweidlem26  46270  fourierdlem112  46462  fsumlesge0  46621  sge0sn  46623  sge0f1o  46626  sge0supre  46633  sge0resplit  46650  sge0reuz  46691  sge0reuzb  46692  aacllem  50046