Metamath Proof Explorer

Theorem measbase

Description: The base set of a measure is a sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measbase ⊢ M ∈ measures ⁡ S → S ∈ ⋃ ran ⁡ sigAlgebra

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ M ∈ measures ⁡ S → S ∈ dom ⁡ measures
2 vex ⊢ s ∈ V
3 ovex ⊢ 0 +∞ ∈ V
4 mapex ⊢ s ∈ V ∧ 0 +∞ ∈ V → m | m : s ⟶ 0 +∞ ∈ V
5 2 3 4 mp2an ⊢ m | m : s ⟶ 0 +∞ ∈ V
6 simp1 ⊢ m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y → m : s ⟶ 0 +∞
7 6 ss2abi ⊢ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y ⊆ m | m : s ⟶ 0 +∞
8 5 7 ssexi ⊢ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y ∈ V
9 df-meas ⊢ measures = s ∈ ⋃ ran ⁡ sigAlgebra ⟼ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
10 8 9 dmmpti ⊢ dom ⁡ measures = ⋃ ran ⁡ sigAlgebra
11 1 10 eleqtrdi ⊢ M ∈ measures ⁡ S → S ∈ ⋃ ran ⁡ sigAlgebra