Theorem sumex 14266

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

Syntax hints:   ∨ wo 382   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897  Vcvv 3173  ⦋csb 3499   ⊆ wss 3540  ifcif 4036   class class class wbr 4583   ↦ cmpt 4643  ℩cio 5766  –1-1-onto→wf1o 5803  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818  ℕcn 10897  ℤcz 11254  ℤ_≥cuz 11563  ...cfz 12197  seqcseq 12663   ⇝ cli 14063  Σcsu 14264

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-sum 14265

This theorem is referenced by:  fsumrlim  14384  fsumo1  14385  efval  14649  efcvgfsum  14655  eftlub  14678  bitsinv2  15003  bitsinv  15008  lebnumlem3  22570  isi1f  23247  itg1val  23256  itg1climres  23287  itgex  23343  itgfsum  23399  dvmptfsum  23542  plyeq0lem  23770  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeid2  23799  plyco  23801  coemullem  23810  coemul  23812  aareccl  23885  aaliou3lem5  23906  aaliou3lem6  23907  aaliou3lem7  23908  taylpval  23925  psercn  23984  pserdvlem2  23986  pserdv  23987  abelthlem6  23994  abelthlem8  23997  abelthlem9  23998  logtayl  24206  leibpi  24469  basellem3  24609  chtval  24636  chpval  24648  sgmval  24668  muinv  24719  dchrvmasumlem1  24984  dchrisum0fval  24994  dchrisum0fno1  25000  dchrisum0lem3  25008  dchrisum0  25009  mulogsum  25021  logsqvma2  25032  selberglem1  25034  pntsval  25061  ecgrtg  25663  esumpcvgval  29467  esumcvg  29475  eulerpartlemsv1  29745  signsplypnf  29953  signsvvfval  29981  fwddifnval  31440  knoppndvlem6  31678  binomcxplemnotnn0  37577  stoweidlem11  38904  stoweidlem26  38919  fourierdlem112  39111  fsumlesge0  39270  sge0sn  39272  sge0f1o  39275  sge0supre  39282  sge0resplit  39299  sge0reuz  39340  sge0reuzb  39341  aacllem  42356