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 )