Theorem voliunsge0

Description: The Lebesgue measure function is countably additive. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	voliunsge0.1	|- ( ph -> E : NN --> dom vol )
	voliunsge0.2	|- ( ph -> Disj_ n e. NN ( E ` n ) )
Assertion	voliunsge0	|- ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		voliunsge0.1	|- ( ph -> E : NN --> dom vol )
2		voliunsge0.2	|- ( ph -> Disj_ n e. NN ( E ` n ) )
3		eqid	|- seq 1 ( + , ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) = seq 1 ( + , ( n e. NN |-> ( vol ` ( E ` n ) ) ) )
4		eqid	|- ( n e. NN |-> ( vol ` ( E ` n ) ) ) = ( n e. NN |-> ( vol ` ( E ` n ) ) )
5	3 4 1 2	voliunsge0lem	|- ( ph -> ( vol ` U_ n e. NN ( E ` n ) ) = ( sum^ ` ( n e. NN |-> ( vol ` ( E ` n ) ) ) ) )