Theorem sumex 15038

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

Syntax hints:   ∧ wa 398   ∨ wo 843   = wceq 1533  ∃wex 1776   ∈ wcel 2110  ∃wrex 3139  Vcvv 3494  ⦋csb 3882   ⊆ wss 3935  ifcif 4466   class class class wbr 5058   ↦ cmpt 5138  ℩cio 6306  –1-1-onto→wf1o 6348  ‘cfv 6349  (class class class)co 7150  0cc0 10531  1c1 10532   + caddc 10534  ℕcn 11632  ℤcz 11975  ℤ_≥cuz 12237  ...cfz 12886  seqcseq 13363   ⇝ cli 14835  Σcsu 15036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4561  df-pr 4563  df-uni 4832  df-iota 6308  df-sum 15037

This theorem is referenced by:  fsumrlim  15160  fsumo1  15161  efval  15427  efcvgfsum  15433  eftlub  15456  bitsinv2  15786  bitsinv  15791  lebnumlem3  23561  isi1f  24269  itg1val  24278  itg1climres  24309  itgex  24365  itgfsum  24421  dvmptfsum  24566  plyeq0lem  24794  plyaddlem1  24797  plymullem1  24798  coeeulem  24808  coeid2  24823  plyco  24825  coemullem  24834  coemul  24836  aareccl  24909  aaliou3lem5  24930  aaliou3lem6  24931  aaliou3lem7  24932  taylpval  24949  psercn  25008  pserdvlem2  25010  pserdv  25011  abelthlem6  25018  abelthlem8  25021  abelthlem9  25022  logtayl  25237  leibpi  25514  basellem3  25654  chtval  25681  chpval  25693  sgmval  25713  muinv  25764  dchrvmasumlem1  26065  dchrisum0fval  26075  dchrisum0fno1  26081  dchrisum0lem3  26089  dchrisum0  26090  mulogsum  26102  logsqvma2  26113  selberglem1  26115  pntsval  26142  ecgrtg  26763  esumpcvgval  31332  esumcvg  31340  eulerpartlemsv1  31609  signsplypnf  31815  signsvvfval  31843  vtsval  31903  circlemeth  31906  fwddifnval  33619  knoppndvlem6  33851  binomcxplemnotnn0  40681  stoweidlem11  42290  stoweidlem26  42305  fourierdlem112  42497  fsumlesge0  42653  sge0sn  42655  sge0f1o  42658  sge0supre  42665  sge0resplit  42682  sge0reuz  42723  sge0reuzb  42724  aacllem  44896