Theorem sumex 15861

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

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1569  ∃wex 1811   ∈ wcel 2144  ∃wrex 3086  Vcvv 3450  ⦋csb 3846   ⊆ wss 3895  ifcif 4481   class class class wbr 5102   ↦ cmpt 5185  ℩cio 6492  –1-1-onto→wf1o 6538  ‘cfv 6539  (class class class)co 7421  0cc0 11204  1c1 11205   + caddc 11207  ℕcn 12339  ℤcz 12697  ℤ_≥cuz 12969  ...cfz 13643  seqcseq 14148   ⇝ cli 15657  Σcsu 15859

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-pr 4587  df-uni 4867  df-iota 6494  df-sum 15860

This theorem is used by:  fsumrlim  15984  fsumo1  15985  efval  16251  efcvgfsum  16258  eftlub  16283  bitsinv2  16619  bitsinv  16624  lebnumlem3  25290  isi1f  26001  itg1val  26010  itg1climres  26041  itgex  26097  itgfsum  26153  dvmptfsum  26301  plyeq0lem  26535  plyaddlem1  26538  plymullem1  26539  coeeulem  26549  coeid2  26564  plyco  26566  coemullem  26575  coemul  26577  aareccl  26659  aaliou3lem5  26680  aaliou3lem6  26681  aaliou3lem7  26682  taylpval  26700  psercn  26759  pserdvlem2  26761  pserdv  26762  abelthlem6  26769  abelthlem8  26772  abelthlem9  26773  logtayl  26994  leibpi  27276  basellem3  27416  chtval  27443  chpval  27455  sgmval  27475  muinv  27526  dchrvmasumlem1  27828  dchrisum0fval  27838  dchrisum0fno1  27844  dchrisum0lem3  27852  dchrisum0  27853  mulogsum  27865  logsqvma2  27876  selberglem1  27878  pntsval  27905  ecgrtg  29567  esumpcvgval  34757  esumcvg  34765  eulerpartlemsv1  35035  signsplypnf  35226  signsvvfval  35254  vtsval  35313  circlemeth  35316  fwddifnval  37021  knoppndvlem6  37476  binomcxplemnotnn0  45434  stoweidlem11  47115  stoweidlem26  47130  fourierdlem112  47322  fsumlesge0  47481  sge0sn  47483  sge0f1o  47486  sge0supre  47493  sge0resplit  47510  sge0reuz  47551  sge0reuzb  47552  aacllem  51108