Theorem voliunsge0

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

	Ref	Expression
Hypotheses	voliunsge0.1	⊢ ( 𝜑 → 𝐸 : ℕ ⟶ dom vol )
	voliunsge0.2	⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
Assertion	voliunsge0	⊢ ( 𝜑 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		voliunsge0.1	⊢ ( 𝜑 → 𝐸 : ℕ ⟶ dom vol )
2		voliunsge0.2	⊢ ( 𝜑 → Disj 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) )
3		eqid	⊢ seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) = seq 1 ( + , ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) )
4		eqid	⊢ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) )
5	3 4 1 2	voliunsge0lem	⊢ ( 𝜑 → ( vol ‘ ∪ 𝑛 ∈ ℕ ( 𝐸 ‘ 𝑛 ) ) = ( Σ^ ‘ ( 𝑛 ∈ ℕ ↦ ( vol ‘ ( 𝐸 ‘ 𝑛 ) ) ) ) )