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∈𝒫sx≼ω∧Disjy∈xy→m⁡⋃x=∑*y∈xm⁡y→m:s⟶0+∞
7 6 ss2abi ⊢m|m:s⟶0+∞∧m⁡∅=0∧∀x∈𝒫sx≼ω∧Disjy∈xy→m⁡⋃x=∑*y∈xm⁡y⊆m|m:s⟶0+∞
8 5 7 ssexi ⊢m|m:s⟶0+∞∧m⁡∅=0∧∀x∈𝒫sx≼ω∧Disjy∈xy→m⁡⋃x=∑*y∈xm⁡y∈V
9 df-meas ⊢measures=s∈⋃ran⁡sigAlgebra⟼m|m:s⟶0+∞∧m⁡∅=0∧∀x∈𝒫sx≼ω∧Disjy∈xy→m⁡⋃x=∑*y∈xm⁡y
10 8 9 dmmpti ⊢dom⁡measures=⋃ran⁡sigAlgebra
11 1 10 eleqtrdi ⊢M∈measures⁡S→S∈⋃ran⁡sigAlgebra