Theorem sumex 15705

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

Syntax hints:   ∧ wa 399   ∨ wo 858   = wceq 1559  ∃wex 1798   ∈ wcel 2141  ∃wrex 3085  Vcvv 3453  ⦋csb 3850   ⊆ wss 3902  ifcif 4477   class class class wbr 5097   ↦ cmpt 5178  ℩cio 6469  –1-1-onto→wf1o 6514  ‘cfv 6515  (class class class)co 7390  0cc0 11066  1c1 11067   + caddc 11069  ℕcn 12203  ℤcz 12561  ℤ_≥cuz 12832  ...cfz 13505  seqcseq 14007   ⇝ cli 15501  Σcsu 15703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5253

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4580  df-pr 4582  df-uni 4863  df-iota 6471  df-sum 15704

This theorem is referenced by:  fsumrlim  15829  fsumo1  15830  efval  16099  efcvgfsum  16106  eftlub  16131  bitsinv2  16467  bitsinv  16472  lebnumlem3  25012  isi1f  25723  itg1val  25732  itg1climres  25763  itgex  25819  itgfsum  25876  dvmptfsum  26024  plyeq0lem  26257  plyaddlem1  26260  plymullem1  26261  coeeulem  26271  coeid2  26286  plyco  26288  coemullem  26297  coemul  26299  aareccl  26377  aaliou3lem5  26398  aaliou3lem6  26399  aaliou3lem7  26400  taylpval  26417  psercn  26476  pserdvlem2  26478  pserdv  26479  abelthlem6  26486  abelthlem8  26489  abelthlem9  26490  logtayl  26712  leibpi  26994  basellem3  27134  chtval  27161  chpval  27173  sgmval  27193  muinv  27244  dchrvmasumlem1  27546  dchrisum0fval  27556  dchrisum0fno1  27562  dchrisum0lem3  27570  dchrisum0  27571  mulogsum  27583  logsqvma2  27594  selberglem1  27596  pntsval  27623  ecgrtg  29140  esumpcvgval  34335  esumcvg  34343  eulerpartlemsv1  34613  signsplypnf  34804  signsvvfval  34832  vtsval  34891  circlemeth  34894  fwddifnval  36473  knoppndvlem6  36915  binomcxplemnotnn0  44892  stoweidlem11  46545  stoweidlem26  46560  fourierdlem112  46752  fsumlesge0  46911  sge0sn  46913  sge0f1o  46916  sge0supre  46923  sge0resplit  46940  sge0reuz  46981  sge0reuzb  46982  aacllem  50382