Theorem sumex 14759

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

Syntax hints:   ∧ wa 385   ∨ wo 874   = wceq 1653  ∃wex 1875   ∈ wcel 2157  ∃wrex 3090  Vcvv 3385  ⦋csb 3728   ⊆ wss 3769  ifcif 4277   class class class wbr 4843   ↦ cmpt 4922  ℩cio 6062  –1-1-onto→wf1o 6100  ‘cfv 6101  (class class class)co 6878  0cc0 10224  1c1 10225   + caddc 10227  ℕcn 11312  ℤcz 11666  ℤ_≥cuz 11930  ...cfz 12580  seqcseq 13055   ⇝ cli 14556  Σcsu 14757

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-nul 4983

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ral 3094  df-rex 3095  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-sn 4369  df-pr 4371  df-uni 4629  df-iota 6064  df-sum 14758

This theorem is referenced by:  fsumrlim  14881  fsumo1  14882  efval  15146  efcvgfsum  15152  eftlub  15175  bitsinv2  15500  bitsinv  15505  lebnumlem3  23090  isi1f  23782  itg1val  23791  itg1climres  23822  itgex  23878  itgfsum  23934  dvmptfsum  24079  plyeq0lem  24307  plyaddlem1  24310  plymullem1  24311  coeeulem  24321  coeid2  24336  plyco  24338  coemullem  24347  coemul  24349  aareccl  24422  aaliou3lem5  24443  aaliou3lem6  24444  aaliou3lem7  24445  taylpval  24462  psercn  24521  pserdvlem2  24523  pserdv  24524  abelthlem6  24531  abelthlem8  24534  abelthlem9  24535  logtayl  24747  leibpi  25021  basellem3  25161  chtval  25188  chpval  25200  sgmval  25220  muinv  25271  dchrvmasumlem1  25536  dchrisum0fval  25546  dchrisum0fno1  25552  dchrisum0lem3  25560  dchrisum0  25561  mulogsum  25573  logsqvma2  25584  selberglem1  25586  pntsval  25613  ecgrtg  26220  esumpcvgval  30656  esumcvg  30664  eulerpartlemsv1  30934  signsplypnf  31145  signsvvfval  31175  vtsval  31235  circlemeth  31238  fwddifnval  32783  knoppndvlem6  33016  binomcxplemnotnn0  39333  stoweidlem11  40967  stoweidlem26  40982  fourierdlem112  41174  fsumlesge0  41333  sge0sn  41335  sge0f1o  41338  sge0supre  41345  sge0resplit  41362  sge0reuz  41403  sge0reuzb  41404  aacllem  43345