Theorem sumex 14418

Description: A sum is a set. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 13-Jun-2019.)

Assertion

Ref	Expression
sumex	|- sum_ k e. A B e. _V

Proof of Theorem sumex

Dummy variables f m n x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-sum 14417	. 2 |- sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
2		iotaex 5868	. 2 |- ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) e. _V
3	1, 2	eqeltri 2697	1 |- sum_ k e. A B e. _V

Syntax hints:   \/ wo 383   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   E.wrex 2913   _Vcvv 3200   [_csb 3533   C_ wss 3574   ifcif 4086   class class class wbr 4653   |-> cmpt 4729   iotacio 5849   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   0cc0 9936   1c1 9937   + caddc 9939   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   ...cfz 12326   seqcseq 12801   ~~> cli 14215   sum_csu 14416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-sum 14417

This theorem is referenced by:  fsumrlim  14543  fsumo1  14544  efval  14810  efcvgfsum  14816  eftlub  14839  bitsinv2  15165  bitsinv  15170  lebnumlem3  22762  isi1f  23441  itg1val  23450  itg1climres  23481  itgex  23537  itgfsum  23593  dvmptfsum  23738  plyeq0lem  23966  plyaddlem1  23969  plymullem1  23970  coeeulem  23980  coeid2  23995  plyco  23997  coemullem  24006  coemul  24008  aareccl  24081  aaliou3lem5  24102  aaliou3lem6  24103  aaliou3lem7  24104  taylpval  24121  psercn  24180  pserdvlem2  24182  pserdv  24183  abelthlem6  24190  abelthlem8  24193  abelthlem9  24194  logtayl  24406  leibpi  24669  basellem3  24809  chtval  24836  chpval  24848  sgmval  24868  muinv  24919  dchrvmasumlem1  25184  dchrisum0fval  25194  dchrisum0fno1  25200  dchrisum0lem3  25208  dchrisum0  25209  mulogsum  25221  logsqvma2  25232  selberglem1  25234  pntsval  25261  ecgrtg  25863  esumpcvgval  30140  esumcvg  30148  eulerpartlemsv1  30418  signsplypnf  30627  signsvvfval  30655  vtsval  30715  circlemeth  30718  fwddifnval  32270  knoppndvlem6  32508  binomcxplemnotnn0  38555  stoweidlem11  40228  stoweidlem26  40243  fourierdlem112  40435  fsumlesge0  40594  sge0sn  40596  sge0f1o  40599  sge0supre  40606  sge0resplit  40623  sge0reuz  40664  sge0reuzb  40665  aacllem  42547