Theorem sumex 15036

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

Syntax hints:   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∃wrex 3107  Vcvv 3441  ⦋csb 3828   ⊆ wss 3881  ifcif 4425   class class class wbr 5030   ↦ cmpt 5110  ℩cio 6281  –1-1-onto→wf1o 6323  ‘cfv 6324  (class class class)co 7135  0cc0 10526  1c1 10527   + caddc 10529  ℕcn 11625  ℤcz 11969  ℤ_≥cuz 12231  ...cfz 12885  seqcseq 13364   ⇝ cli 14833  Σcsu 15034

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-uni 4801  df-iota 6283  df-sum 15035

This theorem is referenced by:  fsumrlim  15158  fsumo1  15159  efval  15425  efcvgfsum  15431  eftlub  15454  bitsinv2  15782  bitsinv  15787  lebnumlem3  23568  isi1f  24278  itg1val  24287  itg1climres  24318  itgex  24374  itgfsum  24430  dvmptfsum  24578  plyeq0lem  24807  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  coeid2  24836  plyco  24838  coemullem  24847  coemul  24849  aareccl  24922  aaliou3lem5  24943  aaliou3lem6  24944  aaliou3lem7  24945  taylpval  24962  psercn  25021  pserdvlem2  25023  pserdv  25024  abelthlem6  25031  abelthlem8  25034  abelthlem9  25035  logtayl  25251  leibpi  25528  basellem3  25668  chtval  25695  chpval  25707  sgmval  25727  muinv  25778  dchrvmasumlem1  26079  dchrisum0fval  26089  dchrisum0fno1  26095  dchrisum0lem3  26103  dchrisum0  26104  mulogsum  26116  logsqvma2  26127  selberglem1  26129  pntsval  26156  ecgrtg  26777  esumpcvgval  31447  esumcvg  31455  eulerpartlemsv1  31724  signsplypnf  31930  signsvvfval  31958  vtsval  32018  circlemeth  32021  fwddifnval  33737  knoppndvlem6  33969  binomcxplemnotnn0  41060  stoweidlem11  42653  stoweidlem26  42668  fourierdlem112  42860  fsumlesge0  43016  sge0sn  43018  sge0f1o  43021  sge0supre  43028  sge0resplit  43045  sge0reuz  43086  sge0reuzb  43087  aacllem  45329