Theorem sumex 15735

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 15734	. 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 2865	1 ⊢ Σ𝑘 ∈ 𝐴 𝐵 ∈ V

Syntax hints:   ∧ wa 400   ∨ wo 860   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∃wrex 3095  Vcvv 3463  ⦋csb 3861   ⊆ wss 3913  ifcif 4489   class class class wbr 5110   ↦ cmpt 5193  ℩cio 6487  –1-1-onto→wf1o 6532  ‘cfv 6533  (class class class)co 7408  0cc0 11096  1c1 11097   + caddc 11099  ℕcn 12229  ℤcz 12587  ℤ_≥cuz 12858  ...cfz 13531  seqcseq 14033   ⇝ cli 15531  Σcsu 15733

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ne 2965  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-sn 4592  df-pr 4594  df-uni 4874  df-iota 6489  df-sum 15734

This theorem is referenced by:  fsumrlim  15859  fsumo1  15860  efval  16129  efcvgfsum  16136  eftlub  16161  bitsinv2  16497  bitsinv  16502  lebnumlem3  25087  isi1f  25798  itg1val  25807  itg1climres  25838  itgex  25894  itgfsum  25951  dvmptfsum  26099  plyeq0lem  26332  plyaddlem1  26335  plymullem1  26336  coeeulem  26346  coeid2  26361  plyco  26363  coemullem  26372  coemul  26374  aareccl  26452  aaliou3lem5  26473  aaliou3lem6  26474  aaliou3lem7  26475  taylpval  26492  psercn  26551  pserdvlem2  26553  pserdv  26554  abelthlem6  26561  abelthlem8  26564  abelthlem9  26565  logtayl  26787  leibpi  27069  basellem3  27209  chtval  27236  chpval  27248  sgmval  27268  muinv  27319  dchrvmasumlem1  27621  dchrisum0fval  27631  dchrisum0fno1  27637  dchrisum0lem3  27645  dchrisum0  27646  mulogsum  27658  logsqvma2  27669  selberglem1  27671  pntsval  27698  ecgrtg  29270  esumpcvgval  34409  esumcvg  34417  eulerpartlemsv1  34687  signsplypnf  34878  signsvvfval  34906  vtsval  34965  circlemeth  34968  fwddifnval  36550  knoppndvlem6  36991  binomcxplemnotnn0  44951  stoweidlem11  46610  stoweidlem26  46625  fourierdlem112  46817  fsumlesge0  46976  sge0sn  46978  sge0f1o  46981  sge0supre  46988  sge0resplit  47005  sge0reuz  47046  sge0reuzb  47047  aacllem  50457