Metamath Proof Explorer


Theorem measbasedom

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

Ref Expression
Assertion measbasedom ( 𝑀 ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )

Proof

Step Hyp Ref Expression
1 isrnmeas ( 𝑀 ran measures → ( dom 𝑀 ran sigAlgebra ∧ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑀 𝑥 ) = Σ* 𝑦𝑥 ( 𝑀𝑦 ) ) ) ) )
2 1 simprd ( 𝑀 ran measures → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑀 𝑥 ) = Σ* 𝑦𝑥 ( 𝑀𝑦 ) ) ) )
3 dmmeas ( 𝑀 ran measures → dom 𝑀 ran sigAlgebra )
4 ismeas ( dom 𝑀 ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ↔ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑀 𝑥 ) = Σ* 𝑦𝑥 ( 𝑀𝑦 ) ) ) ) )
5 3 4 syl ( 𝑀 ran measures → ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) ↔ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑀 𝑥 ) = Σ* 𝑦𝑥 ( 𝑀𝑦 ) ) ) ) )
6 2 5 mpbird ( 𝑀 ran measures → 𝑀 ∈ ( measures ‘ dom 𝑀 ) )
7 elfvunirn ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → 𝑀 ran measures )
8 6 7 impbii ( 𝑀 ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )