P. 384 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 38301-38400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dfsalgen2 38301*	Alternate characterization of the sigma-algebra generated by a set. It is the smallest sigma-algebra, on the same base set, that includes the set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- ( ph -> X e. V )   =>    |- ( ph -> ( (SalGen ` X ) = S <-> ( ( S e. SAlg /\ U. S = U. X /\ X C_ S ) /\ A. y e. SAlg ( ( U. y = U. X /\ X C_ y ) -> S C_ y ) ) ) )
Theorem	salexct3 38302*	An example of a sigma-algebra that's not closed under uncountable union. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )   =>    |- ( S e. SAlg /\ X C_ S /\ -. U. X e. S )
Theorem	salgencntex 38303*	This counterexample shows that df-salgen 38275 needs to require that all containing sigma-algebra have the same base set. Otherwise, the intersection could lead to a set that is not a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- B = ( 0 [,] 1 )   &    |- T = ~P B   &    |- C = ( S i^i T )   &    |- Z = |^| { s e. SAlg | C C_ s }   =>    |- -. Z e. SAlg
Theorem	salgensscntex 38304*	This counterexample shows that the sigma-algebra generated by a set is not the smallest sigma-algebra containing the set, if we consider also sigma-algebras with a larger base set. (Contributed by Glauco Siliprandi, 3-Jan-2021.)
|- A = ( 0 [,] 2 )   &    |- S = { x e. ~P A | ( x ~<_ om \/ ( A \ x ) ~<_ om ) }   &    |- X = ran ( y e. ( 0 [,] 1 ) |-> { y } )   &    |- G = (SalGen ` X )   =>    |- ( X C_ S /\ S e. SAlg /\ -. G C_ S )
Theorem	issalnnd 38305*	Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> S e. V )   &    |- ( ph -> (/) e. S )   &    |- X = U. S   &    |- ( ( ph /\ y e. S ) -> ( X \ y ) e. S )   &    |- ( ( ph /\ e : NN --> S ) -> U_ n e. NN ( e ` n ) e. S )   =>    |- ( ph -> S e. SAlg )
Theorem	dmvolsal 38306	Lebesgue measurable sets form a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- dom vol e. SAlg
21.30.19.2  Sum of nonnegative extended reals
Syntax	csumge0 38307	Extend class notation to include the sum of nonnegative extended reals.
class Σ^
Definition	df-sumge0 38308*	Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.
|- Σ^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )
Theorem	sge0rnre 38309*	When Σ^ is applied to nonnegative real numbers the range used in its definition is a subset of the reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) C_ RR )
Theorem	fge0icoicc 38310	If F maps to nonnegative reals, then F maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> F : X --> ( 0 [,] +oo ) )
Theorem	sge0val 38311*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ( X e. V /\ F : X --> ( 0 [,] +oo ) ) -> (Σ^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( y e. ( ~P X i^i Fin ) |-> sum_ w e. y ( F ` w ) ) , RR* , < ) ) )
Theorem	fge0npnf 38312	If F maps to nonnegative reals, then +oo is not in its range. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> -. +oo e. ran F )
Theorem	sge0rnn0 38313*	The range used in the definition of Σ^ is not empty. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) =/= (/)
Theorem	sge0vald 38314*	The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) )
Theorem	fge0iccico 38315	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> -. +oo e. ran F )   =>    |- ( ph -> F : X --> ( 0 [,) +oo ) )
Theorem	gsumge0cl 38316	Closure of group sum, for finitely supported nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> F finSupp 0 )   =>    |- ( ph -> ( G gsumg F ) e. ( 0 [,] +oo ) )
Theorem	sge0reval 38317*	Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) )
Theorem	sge0pnfval 38318	If a term in the sum of nonnegative extended reals is +oo, then the value of the sum is +oo. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> +oo e. ran F )   =>    |- ( ph -> (Σ^ ` F ) = +oo )
Theorem	fge0iccre 38319	A range of nonnegative extended reals without plus infinity. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> -. +oo e. ran F )   =>    |- ( ph -> F : X --> RR )
Theorem	sge0z 38320*	Any nonnegative extended sum of zero is zero. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> 0 ) ) = 0 )
Theorem	sge00 38321	The sum of nonnegative extended reals is zero when applied to the empty set. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- (Σ^ ` (/) ) = 0
Theorem	fsumlesge0 38322*	Every finite subsum of nonnegative reals is less than or equal to the extended sum over the whole (possibly infinite) domain. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,) +oo ) )   &    |- ( ph -> Y C_ X )   &    |- ( ph -> Y e. Fin )   =>    |- ( ph -> sum_ x e. Y ( F ` x ) <_ (Σ^ ` F ) )
Theorem	sge0revalmpt 38323*	Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) = sup ( ran ( y e. ( ~P A i^i Fin ) |-> sum_ x e. y B ) , RR* , < ) )
Theorem	sge0sn 38324	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : { A } --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = ( F ` A ) )
Theorem	sge0tsms 38325	Σ^ applied to a nonnegative function (its meaningful domain) is the same as the infinite group sum (that's always convergent, in this case). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) e. ( G tsums F ) )
Theorem	sge0cl 38326	The arbitrary sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) e. ( 0 [,] +oo ) )
Theorem	sge0f1o 38327*	Re-index a nonnegative extended sum using a bijection. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- F/ n ph   &    |- ( k = G -> B = D )   &    |- ( ph -> C e. V )   &    |- ( ph -> F : C -1-1-onto-> A )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = (Σ^ ` ( n e. C |-> D ) ) )
Theorem	sge0snmpt 38328*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> C e. ( 0 [,] +oo ) )   &    |- ( k = A -> B = C )   =>    |- ( ph -> (Σ^ ` ( k e. { A } |-> B ) ) = C )
Theorem	sge0ge0 38329	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> 0 <_ (Σ^ ` F ) )
Theorem	sge0xrcl 38330	The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) e. RR* )
Theorem	sge0repnf 38331	The of nonnegative extended reals is a real number if and only if it is not +oo. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> ( (Σ^ ` F ) e. RR <-> -. (Σ^ ` F ) = +oo ) )
Theorem	sge0fsum 38332*	The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. Fin )   &    |- ( ph -> F : X --> ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = sum_ x e. X ( F ` x ) )
Theorem	sge0rern 38333	If the sum of nonnegative extended reals is not +oo then no terms is +oo. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> -. +oo e. ran F )
Theorem	sge0supre 38334*	If the arbitrary sum of nonnegative extended reals is real, then it is the supremum (in the real numbers) of finite subsums. Similar to sge0sup 38336, but here we can use sup with respect to RR instead of RR* (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR , < ) )
Theorem	sge0fsummpt 38335*	The arbitrary sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = sum_ k e. A B )
Theorem	sge0sup 38336*	The arbitrary sum of nonnegative extended reals is the supremum of finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = sup ( ran ( x e. ( ~P X i^i Fin ) |-> (Σ^ ` ( F |` x ) ) ) , RR* , < ) )
Theorem	sge0less 38337	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( F |` Y ) ) <_ (Σ^ ` F ) )
Theorem	sge0rnbnd 38338*	The range used in the definition of Σ^ is bounded, when the whole sum is a real number. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> E. z e. RR A. w e. ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) w <_ z )
Theorem	sge0pr 38339*	Sum of a pair of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. ( 0 [,] +oo ) )   &    |- ( ph -> E e. ( 0 [,] +oo ) )   &    |- ( k = A -> C = D )   &    |- ( k = B -> C = E )   &    |- ( ph -> A =/= B )   =>    |- ( ph -> (Σ^ ` ( k e. { A , B } |-> C ) ) = ( D +e E ) )
Theorem	sge0gerp 38340*	The arbitrary sum of nonnegative extended reals is larger or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. RR* )   &    |- ( ( ph /\ x e. RR+ ) -> E. z e. ( ~P X i^i Fin ) A <_ ( (Σ^ ` ( F |` z ) ) +e x ) )   =>    |- ( ph -> A <_ (Σ^ ` F ) )
Theorem	sge0pnffigt 38341*	If the sum of nonnegative extended reals is +oo, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) = +oo )   &    |- ( ph -> Y e. RR )   =>    |- ( ph -> E. x e. ( ~P X i^i Fin ) Y < (Σ^ ` ( F |` x ) ) )
Theorem	sge0ssre 38342	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> (Σ^ ` ( F |` Y ) ) e. RR )
Theorem	sge0lefi 38343*	A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> A e. RR* )   =>    |- ( ph -> ( (Σ^ ` F ) <_ A <-> A. x e. ( ~P X i^i Fin ) (Σ^ ` ( F |` x ) ) <_ A ) )
Theorem	sge0lessmpt 38344*	A shorter sum of nonnegative extended reals is smaller than a longer one. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> (Σ^ ` ( x e. C |-> B ) ) <_ (Σ^ ` ( x e. A |-> B ) ) )
Theorem	sge0ltfirp 38345*	If the sum of nonnegative extended reals is real, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> Y e. RR+ )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> E. x e. ( ~P X i^i Fin ) (Σ^ ` F ) < ( (Σ^ ` ( F |` x ) ) + Y ) )
Theorem	sge0prle 38346*	The sum of a pair of nonnegative extended reals is less than or equal their extended addition. When it is a distinct pair, than equality holds, see sge0pr 38339. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> D e. ( 0 [,] +oo ) )   &    |- ( ph -> E e. ( 0 [,] +oo ) )   &    |- ( k = A -> C = D )   &    |- ( k = B -> C = E )   =>    |- ( ph -> (Σ^ ` ( k e. { A , B } |-> C ) ) <_ ( D +e E ) )
Theorem	sge0gerpmpt 38347*	The arbitrary sum of nonnegative extended reals is larger or equal to a given extended real number if this number can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. RR* )   &    |- ( ( ph /\ y e. RR+ ) -> E. z e. ( ~P A i^i Fin ) C <_ ( (Σ^ ` ( x e. z |-> B ) ) +e y ) )   =>    |- ( ph -> C <_ (Σ^ ` ( x e. A |-> B ) ) )
Theorem	sge0resrnlem 38348	The sum of nonnegative extended reals restricted to the range of a function is less or equal to the sum of the composition of the two functions. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : B --> ( 0 [,] +oo ) )   &    |- ( ph -> G : A --> B )   &    |- ( ph -> X e. ~P A )   &    |- ( ph -> ( G |` X ) : X -1-1-onto-> ran G )   =>    |- ( ph -> (Σ^ ` ( F |` ran G ) ) <_ (Σ^ ` ( F o. G ) ) )
Theorem	sge0resrn 38349	The sum of nonnegative extended reals restricted to the range of a function is less or equal to the sum of the composition of the two functions (well order hypothesis allows to avoid using the axiom of choice). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : B --> ( 0 [,] +oo ) )   &    |- ( ph -> G : A --> B )   &    |- ( ph -> R We A )   =>    |- ( ph -> (Σ^ ` ( F |` ran G ) ) <_ (Σ^ ` ( F o. G ) ) )
Theorem	sge0ssrempt 38350*	If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. RR )   &    |- ( ph -> C C_ A )   =>    |- ( ph -> (Σ^ ` ( x e. C |-> B ) ) e. RR )
Theorem	sge0resplit 38351	Σ^ splits into two parts, when it's a real number. This is a special case of sge0split 38354. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- U = ( A u. B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> F : U --> ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` F ) e. RR )   =>    |- ( ph -> (Σ^ ` F ) = ( (Σ^ ` ( F |` A ) ) + (Σ^ ` ( F |` B ) ) ) )
Theorem	sge0le 38352*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X e. V )   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> G : X --> ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. X ) -> ( F ` x ) <_ ( G ` x ) )   =>    |- ( ph -> (Σ^ ` F ) <_ (Σ^ ` G ) )
Theorem	sge0ltfirpmpt 38353*	If the extended sum of nonnegative reals is not +oo, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> Y e. RR+ )   &    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. RR )   =>    |- ( ph -> E. y e. ( ~P A i^i Fin ) (Σ^ ` ( x e. A |-> B ) ) < ( (Σ^ ` ( x e. y |-> B ) ) + Y ) )
Theorem	sge0split 38354	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- U = ( A u. B )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ph -> F : U --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) = ( (Σ^ ` ( F |` A ) ) +e (Σ^ ` ( F |` B ) ) ) )
Theorem	sge0lempt 38355*	If all of the terms of sums compare, so do the sums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. A ) -> B <_ C )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) <_ (Σ^ ` ( x e. A |-> C ) ) )
Theorem	sge0splitmpt 38356*	Split a sum of nonnegative extended reals into two parts. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> ( A i^i B ) = (/) )   &    |- ( ( ph /\ x e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. B ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( x e. ( A u. B ) |-> C ) ) = ( (Σ^ ` ( x e. A |-> C ) ) +e (Σ^ ` ( x e. B |-> C ) ) ) )
Theorem	sge0ss 38357*	Change the index set to a subset in a sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- ( ph -> B e. V )   &    |- ( ph -> A C_ B )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. ( B \ A ) ) -> C = 0 )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> C ) ) = (Σ^ ` ( k e. B |-> C ) ) )
Theorem	sge0iunmptlemfi 38358*	Sum of nonnegative extended reals over a disjoint indexed union (in this lemma, for a finite index set). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. Fin )   &    |- ( ( ph /\ x e. A ) -> B e. V )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. A ) -> (Σ^ ` ( k e. B |-> C ) ) e. RR )   =>    |- ( ph -> (Σ^ ` ( k e. U_ x e. A B |-> C ) ) = (Σ^ ` ( x e. A |-> (Σ^ ` ( k e. B |-> C ) ) ) ) )
Theorem	sge0p1 38359*	The addition of the next term in a finite sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> N e. ( ZZ>= ` M ) )   &    |- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. ( 0 [,] +oo ) )   &    |- ( k = ( N + 1 ) -> A = B )   =>    |- ( ph -> (Σ^ ` ( k e. ( M ... ( N + 1 ) ) |-> A ) ) = ( (Σ^ ` ( k e. ( M ... N ) |-> A ) ) +e B ) )
Theorem	sge0iunmptlemre 38360*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ x e. A ) -> (Σ^ ` ( k e. B |-> C ) ) e. RR )   &    |- ( ph -> (Σ^ ` ( k e. U_ x e. A B |-> C ) ) e. RR* )   &    |- ( ph -> (Σ^ ` ( x e. A |-> (Σ^ ` ( k e. B |-> C ) ) ) ) e. RR* )   &    |- ( ph -> ( k e. U_ x e. A B |-> C ) : U_ x e. A B --> ( 0 [,] +oo ) )   &    |- ( ph -> U_ x e. A B e. _V )   =>    |- ( ph -> (Σ^ ` ( k e. U_ x e. A B |-> C ) ) = (Σ^ ` ( x e. A |-> (Σ^ ` ( k e. B |-> C ) ) ) ) )
Theorem	sge0fodjrnlem 38361*	Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- F/ n ph   &    |- ( k = G -> B = D )   &    |- ( ph -> C e. V )   &    |- ( ph -> F : C -onto-> A )   &    |- ( ph -> Disj n e. C ( F ` n ) )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k = (/) ) -> B = 0 )   &    |- Z = ( `' F " { (/) } )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = (Σ^ ` ( n e. C |-> D ) ) )
Theorem	sge0fodjrn 38362*	Re-index a nonnegative extended sum using an onto function with disjoint range, when the empty set is assigned 0 in the sum (this is true, for example, both for measures and outer measures). (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- F/ n ph   &    |- ( k = G -> B = D )   &    |- ( ph -> C e. V )   &    |- ( ph -> F : C -onto-> A )   &    |- ( ph -> Disj n e. C ( F ` n ) )   &    |- ( ( ph /\ n e. C ) -> ( F ` n ) = G )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k = (/) ) -> B = 0 )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = (Σ^ ` ( n e. C |-> D ) ) )
Theorem	sge0iunmpt 38363*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- ( ph -> Disj x e. A B )   &    |- ( ( ph /\ x e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. U_ x e. A B |-> C ) ) = (Σ^ ` ( x e. A |-> (Σ^ ` ( k e. B |-> C ) ) ) ) )
Theorem	sge0iun 38364*	Sum of nonnegative extended reals over a disjoint indexed union. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. W )   &    |- X = U_ x e. A B   &    |- ( ph -> F : X --> ( 0 [,] +oo ) )   &    |- ( ph -> Disj x e. A B )   =>    |- ( ph -> (Σ^ ` F ) = (Σ^ ` ( x e. A |-> (Σ^ ` ( F |` B ) ) ) ) )
Theorem	sge0nemnf 38365	The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> F : A --> ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` F ) =/= -oo )
Theorem	sge0rpcpnf 38366*	The sum of an infinite number of a positive constant, is +oo (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ph -> -. A e. Fin )   &    |- ( ph -> B e. RR+ )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) = +oo )
Theorem	sge0rernmpt 38367*	If the sum of nonnegative extended reals is not +oo then no term is +oo. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. RR )   =>    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,) +oo ) )
Theorem	sge0lefimpt 38368*	A sum of nonnegative extended reals is smaller than a given extended real if and only if every finite subsum is smaller than it. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> C e. RR* )   =>    |- ( ph -> ( (Σ^ ` ( x e. A |-> B ) ) <_ C <-> A. y e. ( ~P A i^i Fin ) (Σ^ ` ( x e. y |-> B ) ) <_ C ) )
Theorem	nn0ssge0 38369	Nonnegative integers are nonnegative reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- NN0 C_ ( 0 [,) +oo )
Theorem	sge0clmpt 38370*	The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. ( 0 [,] +oo ) )
Theorem	sge0ltfirpmpt2 38371*	If the extended sum of nonnegative reals is not +oo, then it can be approximated from below by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> Y e. RR+ )   &    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. RR )   =>    |- ( ph -> E. y e. ( ~P A i^i Fin ) (Σ^ ` ( x e. A |-> B ) ) < ( sum_ x e. y B + Y ) )
Theorem	sge0isum 38372	If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> ( 0 [,) +oo ) )   &    |- G = seq M ( + , F )   &    |- ( ph -> G ~~> B )   =>    |- ( ph -> (Σ^ ` F ) = B )
Theorem	sge0xrclmpt 38373*	The generalized sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ x ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ x e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( x e. A |-> B ) ) e. RR* )
Theorem	sge0xp 38374*	Combine two generalized sums of nonnegative extended reals into a single generalized sum over the cartesian product. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( z = <. j , k >. -> D = C )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ( ph /\ j e. A /\ k e. B ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( j e. A |-> (Σ^ ` ( k e. B |-> C ) ) ) ) = (Σ^ ` ( z e. ( A X. B ) |-> D ) ) )
Theorem	sge0isummpt 38375*	If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ( ph /\ k e. Z ) -> A e. ( 0 [,) +oo ) )   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> seq M ( + , ( k e. Z |-> A ) ) ~~> B )   =>    |- ( ph -> (Σ^ ` ( k e. Z |-> A ) ) = B )
Theorem	sge0ad2en 38376*	The value of the infinite geometric series 2 ^ -u 1 + 2 ^ -u 2 +... , multiplied by a constant. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` ( n e. NN |-> ( A / ( 2 ^ n ) ) ) ) = A )
Theorem	sge0isummpt2 38377*	If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ( ph /\ k e. Z ) -> A e. ( 0 [,) +oo ) )   &    |- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> seq M ( + , ( k e. Z |-> A ) ) ~~> B )   =>    |- ( ph -> (Σ^ ` ( k e. Z |-> A ) ) = sum_ k e. Z A )
Theorem	sge0xaddlem1 38378*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> E e. RR+ )   &    |- ( ph -> U C_ A )   &    |- ( ph -> U e. Fin )   &    |- ( ph -> W C_ A )   &    |- ( ph -> W e. Fin )   &    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) < ( sum_ k e. U B + ( E / 2 ) ) )   &    |- ( ph -> (Σ^ ` ( k e. A |-> C ) ) < ( sum_ k e. W C + ( E / 2 ) ) )   &    |- ( ph -> sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) e. ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) e. RR )   &    |- ( ph -> (Σ^ ` ( k e. A |-> C ) ) e. RR )   =>    |- ( ph -> ( (Σ^ ` ( k e. A |-> B ) ) + (Σ^ ` ( k e. A |-> C ) ) ) <_ ( sup ( ran ( x e. ( ~P A i^i Fin ) |-> sum_ k e. x ( B + C ) ) , RR* , < ) +e E ) )
Theorem	sge0xaddlem2 38379*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,) +oo ) )   &    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) e. RR )   &    |- ( ph -> (Σ^ ` ( k e. A |-> C ) ) e. RR )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> ( B +e C ) ) ) = ( (Σ^ ` ( k e. A |-> B ) ) +e (Σ^ ` ( k e. A |-> C ) ) ) )
Theorem	sge0xadd 38380*	The extended addition of two generalized sums of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> ( B +e C ) ) ) = ( (Σ^ ` ( k e. A |-> B ) ) +e (Σ^ ` ( k e. A |-> C ) ) ) )
Theorem	sge0fsummptf 38381*	The generalized sum of a finite set of nonnegative extended real numbers is equal to the sum of those numbers, when none of them is +oo (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. Fin )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = sum_ k e. A B )
Theorem	sge0snmptf 38382*	A sum of a nonnegative extended real is the term. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ph -> C e. ( 0 [,] +oo ) )   &    |- ( k = A -> B = C )   =>    |- ( ph -> (Σ^ ` ( k e. { A } |-> B ) ) = C )
Theorem	sge0ge0mpt 38383*	The sum of nonnegative extended reals is nonnegative. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> 0 <_ (Σ^ ` ( k e. A |-> B ) ) )
Theorem	sge0repnfmpt 38384*	The of nonnegative extended reals is a real number if and only if it is not +oo. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   =>    |- ( ph -> ( (Σ^ ` ( k e. A |-> B ) ) e. RR <-> -. (Σ^ ` ( k e. A |-> B ) ) = +oo ) )
Theorem	sge0pnffigtmpt 38385*	If the generalized sum of nonnegative reals is +oo, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = +oo )   &    |- ( ph -> Y e. RR )   =>    |- ( ph -> E. x e. ( ~P A i^i Fin ) Y < (Σ^ ` ( k e. x |-> B ) ) )
Theorem	sge0splitsn 38386*	Separate out a term in a generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. W )   &    |- ( ph -> -. B e. A )   &    |- ( ( ph /\ k e. A ) -> C e. ( 0 [,] +oo ) )   &    |- ( k = B -> C = D )   &    |- ( ph -> D e. ( 0 [,] +oo ) )   =>    |- ( ph -> (Σ^ ` ( k e. ( A u. { B } ) |-> C ) ) = ( (Σ^ ` ( k e. A |-> C ) ) +e D ) )
Theorem	sge0pnffsumgt 38387*	If the sum of nonnegative extended reals is +oo, then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   &    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = +oo )   &    |- ( ph -> Y e. RR )   =>    |- ( ph -> E. x e. ( ~P A i^i Fin ) Y < sum_ k e. x B )
Theorem	sge0gtfsumgt 38388*	If the generalized sum of nonnegative reals is larger than a given number, then that number can be dominated by a finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,) +oo ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < (Σ^ ` ( k e. A |-> B ) ) )   =>    |- ( ph -> E. y e. ( ~P A i^i Fin ) C < sum_ k e. y B )
Theorem	sge0uzfsumgt 38389*	If a real number is smaller than a generalized sum of nonnegative reals, then it is smaller than some finite subsum. (Contributed by Glauco Siliprandi, 21-Nov-2020.)
|- F/ k ph   &    |- ( ph -> K e. ZZ )   &    |- Z = ( ZZ>= ` K )   &    |- ( ( ph /\ k e. Z ) -> B e. ( 0 [,) +oo ) )   &    |- ( ph -> C e. RR )   &    |- ( ph -> C < (Σ^ ` ( k e. Z |-> B ) ) )   =>    |- ( ph -> E. m e. Z C < sum_ k e. ( K ... m ) B )
Theorem	sge0pnfmpt 38390*	If a term in the sum of nonnegative extended reals is +oo, then the value of the sum is +oo (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- F/ k ph   &    |- ( ph -> A e. V )   &    |- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )   &    |- ( ph -> E. k e. A B = +oo )   =>    |- ( ph -> (Σ^ ` ( k e. A |-> B ) ) = +oo )
Theorem	sge0seq 38391	A series of nonnegative reals agrees with the generalized sum of nonnegative reals. (Contributed by Glauco Siliprandi, 3-Mar-2021.)
|- ( ph -> M e. ZZ )   &    |- Z = ( ZZ>= ` M )   &    |- ( ph -> F : Z --> ( 0 [,) +oo ) )   &    |- G = seq M ( + , F )   =>    |- ( ph -> (Σ^ ` F ) = sup ( ran G , RR* , < ) )
21.30.19.3  Measures Proofs for most of the theorems in section 112 of [Fremlin1]
Syntax	cmea 38392	Extend class notation with the class of measures.
class Meas
Definition	df-mea 38393*	Define the class of measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- Meas = { x | ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x e. SAlg ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P dom x ( ( y ~<_ om /\ Disj w e. y w ) -> ( x ` U. y ) = (Σ^ ` ( x |` y ) ) ) ) }
Theorem	ismea 38394*	Express the predicate " M is a measure." Definition 112A of [Fremlin1] p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. x e. ~P dom M ( ( x ~<_ om /\ Disj y e. x y ) -> ( M ` U. x ) = (Σ^ ` ( M |` x ) ) ) ) )
Theorem	dmmeasal 38395	The domain of a measure is a sigma-algebra. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. Meas )   &    |- S = dom M   =>    |- ( ph -> S e. SAlg )
Theorem	meaf 38396	A measure is a function that maps to nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. Meas )   &    |- S = dom M   =>    |- ( ph -> M : S --> ( 0 [,] +oo ) )
Theorem	mea0 38397	The measure of the empty set is always 0 . (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. Meas )   =>    |- ( ph -> ( M ` (/) ) = 0 )
Theorem	nnfoctbdjlem 38398*	There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> A C_ NN )   &    |- ( ph -> G : A -1-1-onto-> X )   &    |- ( ph -> Disj y e. X y )   &    |- F = ( n e. NN |-> if ( ( n = 1 \/ -. ( n - 1 ) e. A ) , (/) , ( G ` ( n - 1 ) ) ) )   =>    |- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )
Theorem	nnfoctbdj 38399*	There exists a mapping from NN onto any (nonempty) countable set of disjoint sets, such that elements in the range of the map are disjoint. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> X ~<_ om )   &    |- ( ph -> X =/= (/) )   &    |- ( ph -> Disj y e. X y )   =>    |- ( ph -> E. f ( f : NN -onto-> ( X u. { (/) } ) /\ Disj n e. NN ( f ` n ) ) )
Theorem	meadjuni 38400*	The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
|- ( ph -> M e. Meas )   &    |- S = dom M   &    |- ( ph -> X C_ S )   &    |- ( ph -> X ~<_ om )   &    |- ( ph -> Disj x e. X x )   =>    |- ( ph -> ( M ` U. X ) = (Σ^ ` ( M |` X ) ) )