Metamath Proof Explorer


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 ‘ ( 𝐸𝑛 ) ) ) ) )