Theorem sumex 15775

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 15774	. 2 ⊢ Σ𝑘 ∈ 𝐴 𝐵 = (℩𝑥(∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , (𝑛 ∈ ℤ ↦ if(𝑛 ∈ 𝐴, ⦋𝑛 / 𝑘⦌𝐵, 0))) ⇝ 𝑥) ∨ ∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑥 = (seq1( + , (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵))‘𝑚))))
2		iotaex 6509	. 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 1570  ∃wex 1812   ∈ wcel 2145  ∃wrex 3086  Vcvv 3450  ⦋csb 3847   ⊆ wss 3899  ifcif 4482   class class class wbr 5103   ↦ cmpt 5186  ℩cio 6487  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7413  0cc0 11124  1c1 11125   + caddc 11127  ℕcn 12257  ℤcz 12615  ℤ_≥cuz 12887  ...cfz 13561  seqcseq 14065   ⇝ cli 15571  Σcsu 15773

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5263

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 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6489  df-sum 15774

This theorem is used by:  fsumrlim  15898  fsumo1  15899  efval  16165  efcvgfsum  16172  eftlub  16197  bitsinv2  16533  bitsinv  16538  lebnumlem3  25191  isi1f  25902  itg1val  25911  itg1climres  25942  itgex  25998  itgfsum  26054  dvmptfsum  26202  plyeq0lem  26436  plyaddlem1  26439  plymullem1  26440  coeeulem  26450  coeid2  26465  plyco  26467  coemullem  26476  coemul  26478  aareccl  26562  aaliou3lem5  26583  aaliou3lem6  26584  aaliou3lem7  26585  taylpval  26603  psercn  26662  pserdvlem2  26664  pserdv  26665  abelthlem6  26672  abelthlem8  26675  abelthlem9  26676  logtayl  26897  leibpi  27179  basellem3  27319  chtval  27346  chpval  27358  sgmval  27378  muinv  27429  dchrvmasumlem1  27731  dchrisum0fval  27741  dchrisum0fno1  27747  dchrisum0lem3  27755  dchrisum0  27756  mulogsum  27768  logsqvma2  27779  selberglem1  27781  pntsval  27808  ecgrtg  29440  esumpcvgval  34588  esumcvg  34596  eulerpartlemsv1  34867  signsplypnf  35058  signsvvfval  35086  vtsval  35145  circlemeth  35148  fwddifnval  36743  knoppndvlem6  37214  binomcxplemnotnn0  45180  stoweidlem11  46839  stoweidlem26  46854  fourierdlem112  47046  fsumlesge0  47205  sge0sn  47207  sge0f1o  47210  sge0supre  47217  sge0resplit  47234  sge0reuz  47275  sge0reuzb  47276  aacllem  50772