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 ⊢ φ → E : ℕ ⟶ dom ⁡ vol
voliunsge0.2 ⊢ φ → Disj n ∈ ℕ E ⁡ n
Assertion voliunsge0 ⊢ φ → vol ⁡ ⋃ n ∈ ℕ E ⁡ n = sum^ ⁡ n ∈ ℕ ⟼ vol ⁡ E ⁡ n

Proof

Step Hyp Ref Expression
1 voliunsge0.1 ⊢ φ → E : ℕ ⟶ dom ⁡ vol
2 voliunsge0.2 ⊢ φ → Disj n ∈ ℕ E ⁡ n
3 eqid ⊢ seq 1 + n ∈ ℕ ⟼ vol ⁡ E ⁡ n = seq 1 + n ∈ ℕ ⟼ vol ⁡ E ⁡ n
4 eqid ⊢ n ∈ ℕ ⟼ vol ⁡ E ⁡ n = n ∈ ℕ ⟼ vol ⁡ E ⁡ n
5 3 4 1 2 voliunsge0lem ⊢ φ → vol ⁡ ⋃ n ∈ ℕ E ⁡ n = sum^ ⁡ n ∈ ℕ ⟼ vol ⁡ E ⁡ n