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 ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ran sigAlgebra )

Proof

Step Hyp Ref Expression
1 elfvdm ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ∈ dom measures )
2 vex 𝑠 ∈ V
3 ovex ( 0 [,] +∞ ) ∈ V
4 mapex ( ( 𝑠 ∈ V ∧ ( 0 [,] +∞ ) ∈ V ) → { 𝑚𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V )
5 2 3 4 mp2an { 𝑚𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V
6 simp1 ( ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) → 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) )
7 6 ss2abi { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } ⊆ { 𝑚𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) }
8 5 7 ssexi { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } ∈ V
9 df-meas measures = ( 𝑠 ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } )
10 8 9 dmmpti dom measures = ran sigAlgebra
11 1 10 eleqtrdi ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ran sigAlgebra )