Theorem sumex 15741

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

Syntax hints:   ∧ wa 400   ∨ wo 860   = wceq 1570  ∃wex 1809   ∈ wcel 2143  ∃wrex 3089  Vcvv 3455  ⦋csb 3854   ⊆ wss 3906  ifcif 4488   class class class wbr 5110   ↦ cmpt 5193  ℩cio 6492  –1-1-onto→wf1o 6537  ‘cfv 6538  (class class class)co 7412  0cc0 11101  1c1 11102   + caddc 11104  ℕcn 12234  ℤcz 12592  ℤ_≥cuz 12863  ...cfz 13536  seqcseq 14039   ⇝ cli 15537  Σcsu 15739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-sn 4591  df-pr 4593  df-uni 4874  df-iota 6494  df-sum 15740

This theorem is referenced by:  fsumrlim  15865  fsumo1  15866  efval  16134  efcvgfsum  16141  eftlub  16166  bitsinv2  16502  bitsinv  16507  lebnumlem3  25103  isi1f  25814  itg1val  25823  itg1climres  25854  itgex  25910  itgfsum  25967  dvmptfsum  26115  plyeq0lem  26348  plyaddlem1  26351  plymullem1  26352  coeeulem  26362  coeid2  26377  plyco  26379  coemullem  26388  coemul  26390  aareccl  26470  aaliou3lem5  26491  aaliou3lem6  26492  aaliou3lem7  26493  taylpval  26511  psercn  26570  pserdvlem2  26572  pserdv  26573  abelthlem6  26580  abelthlem8  26583  abelthlem9  26584  logtayl  26806  leibpi  27088  basellem3  27228  chtval  27255  chpval  27267  sgmval  27287  muinv  27338  dchrvmasumlem1  27640  dchrisum0fval  27650  dchrisum0fno1  27656  dchrisum0lem3  27664  dchrisum0  27665  mulogsum  27677  logsqvma2  27688  selberglem1  27690  pntsval  27717  ecgrtg  29314  esumpcvgval  34449  esumcvg  34457  eulerpartlemsv1  34727  signsplypnf  34918  signsvvfval  34946  vtsval  35005  circlemeth  35008  fwddifnval  36636  knoppndvlem6  37087  binomcxplemnotnn0  45049  stoweidlem11  46708  stoweidlem26  46723  fourierdlem112  46915  fsumlesge0  47074  sge0sn  47076  sge0f1o  47079  sge0supre  47086  sge0resplit  47103  sge0reuz  47144  sge0reuzb  47145  aacllem  50584