Theorem sumex 15650

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

Syntax hints:   ∧ wa 395   ∨ wo 848   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ∃wrex 3061  Vcvv 3429  ⦋csb 3837   ⊆ wss 3889  ifcif 4466   class class class wbr 5085   ↦ cmpt 5166  ℩cio 6452  –1-1-onto→wf1o 6497  ‘cfv 6498  (class class class)co 7367  0cc0 11038  1c1 11039   + caddc 11041  ℕcn 12174  ℤcz 12524  ℤ_≥cuz 12788  ...cfz 13461  seqcseq 13963   ⇝ cli 15446  Σcsu 15648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-sum 15649

This theorem is referenced by:  fsumrlim  15774  fsumo1  15775  efval  16044  efcvgfsum  16051  eftlub  16076  bitsinv2  16412  bitsinv  16417  lebnumlem3  24930  isi1f  25641  itg1val  25650  itg1climres  25681  itgex  25737  itgfsum  25794  dvmptfsum  25942  plyeq0lem  26175  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeid2  26204  plyco  26206  coemullem  26215  coemul  26217  aareccl  26292  aaliou3lem5  26313  aaliou3lem6  26314  aaliou3lem7  26315  taylpval  26332  psercn  26391  pserdvlem2  26393  pserdv  26394  abelthlem6  26401  abelthlem8  26404  abelthlem9  26405  logtayl  26624  leibpi  26906  basellem3  27046  chtval  27073  chpval  27085  sgmval  27105  muinv  27156  dchrvmasumlem1  27458  dchrisum0fval  27468  dchrisum0fno1  27474  dchrisum0lem3  27482  dchrisum0  27483  mulogsum  27495  logsqvma2  27506  selberglem1  27508  pntsval  27535  ecgrtg  29052  esumpcvgval  34222  esumcvg  34230  eulerpartlemsv1  34500  signsplypnf  34694  signsvvfval  34722  vtsval  34781  circlemeth  34784  fwddifnval  36345  knoppndvlem6  36777  binomcxplemnotnn0  44783  stoweidlem11  46439  stoweidlem26  46454  fourierdlem112  46646  fsumlesge0  46805  sge0sn  46807  sge0f1o  46810  sge0supre  46817  sge0resplit  46834  sge0reuz  46875  sge0reuzb  46876  aacllem  50276