Theorem sumex 15896

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

This proof depends on syntax axioms:   ∧ wa 401   ∨ wo 861   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃wrex 3090  Vcvv 3454  ⦋csb 3851   ⊆ wss 3900  ifcif 4485   class class class wbr 5106   ↦ cmpt 5190  ℩cio 6516  ⟶1-1ontowf1o 6563  ‘cfv 6564  (class class class)co 7449  0cc0 11237  1c1 11238   + caddc 11240  ℕcn 12373  ℤcz 12731  ℤ_≥cuz 13003  ...cfz 13677  seqcseq 14182   ⇝ cli 15692  Σcsu 15894

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6518  df-sum 15895

This theorem is used by:  fsumrlim  16019  fsumo1  16020  efval  16286  efcvgfsum  16293  eftlub  16318  bitsinv2  16654  bitsinv  16659  lebnumlem3  25328  isi1f  26039  itg1val  26048  itg1climres  26079  itgex  26135  itgfsum  26191  dvmptfsum  26339  plyeq0lem  26573  plyaddlem1  26576  plymullem1  26577  coeeulem  26587  coeid2  26602  plyco  26604  coemullem  26613  coemul  26615  aareccl  26699  aaliou3lem5  26720  aaliou3lem6  26721  aaliou3lem7  26722  taylpval  26740  psercn  26799  pserdvlem2  26801  pserdv  26802  abelthlem6  26809  abelthlem8  26812  abelthlem9  26813  logtayl  27034  leibpi  27316  basellem3  27456  chtval  27483  chpval  27495  sgmval  27515  muinv  27566  dchrvmasumlem1  27868  dchrisum0fval  27878  dchrisum0fno1  27884  dchrisum0lem3  27892  dchrisum0  27893  mulogsum  27905  logsqvma2  27916  selberglem1  27918  pntsval  27945  ecgrtg  29607  esumpcvgval  34814  esumcvg  34822  eulerpartlemsv1  35092  signsplypnf  35283  signsvvfval  35311  vtsval  35370  circlemeth  35373  fwddifnval  37136  knoppndvlem6  37591  binomcxplemnotnn0  45595  stoweidlem11  47288  stoweidlem26  47303  fourierdlem112  47495  fsumlesge0  47654  sge0sn  47656  sge0f1o  47659  sge0supre  47666  sge0resplit  47683  sge0reuz  47724  sge0reuzb  47725  aacllem  51361