Theorem sumex 14615

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

Syntax hints:   ∨ wo 382   ∧ wa 383   = wceq 1630  ∃wex 1851   ∈ wcel 2137  ∃wrex 3049  Vcvv 3338  ⦋csb 3672   ⊆ wss 3713  ifcif 4228   class class class wbr 4802   ↦ cmpt 4879  ℩cio 6008  –1-1-onto→wf1o 6046  ‘cfv 6047  (class class class)co 6811  0cc0 10126  1c1 10127   + caddc 10129  ℕcn 11210  ℤcz 11567  ℤ_≥cuz 11877  ...cfz 12517  seqcseq 12993   ⇝ cli 14412  Σcsu 14613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-nul 4939

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ral 3053  df-rex 3054  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-sn 4320  df-pr 4322  df-uni 4587  df-iota 6010  df-sum 14614

This theorem is referenced by:  fsumrlim  14740  fsumo1  14741  efval  15007  efcvgfsum  15013  eftlub  15036  bitsinv2  15365  bitsinv  15370  lebnumlem3  22961  isi1f  23638  itg1val  23647  itg1climres  23678  itgex  23734  itgfsum  23790  dvmptfsum  23935  plyeq0lem  24163  plyaddlem1  24166  plymullem1  24167  coeeulem  24177  coeid2  24192  plyco  24194  coemullem  24203  coemul  24205  aareccl  24278  aaliou3lem5  24299  aaliou3lem6  24300  aaliou3lem7  24301  taylpval  24318  psercn  24377  pserdvlem2  24379  pserdv  24380  abelthlem6  24387  abelthlem8  24390  abelthlem9  24391  logtayl  24603  leibpi  24866  basellem3  25006  chtval  25033  chpval  25045  sgmval  25065  muinv  25116  dchrvmasumlem1  25381  dchrisum0fval  25391  dchrisum0fno1  25397  dchrisum0lem3  25405  dchrisum0  25406  mulogsum  25418  logsqvma2  25429  selberglem1  25431  pntsval  25458  ecgrtg  26060  esumpcvgval  30447  esumcvg  30455  eulerpartlemsv1  30725  signsplypnf  30934  signsvvfval  30962  vtsval  31022  circlemeth  31025  fwddifnval  32574  knoppndvlem6  32812  binomcxplemnotnn0  39055  stoweidlem11  40729  stoweidlem26  40744  fourierdlem112  40936  fsumlesge0  41095  sge0sn  41097  sge0f1o  41100  sge0supre  41107  sge0resplit  41124  sge0reuz  41165  sge0reuzb  41166  aacllem  43058