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 ⊢ M ∈ ⋃ ran ⁡ measures ↔ M ∈ measures ⁡ dom ⁡ M

Proof

Step Hyp Ref Expression
1 isrnmeas ⊢ M ∈ ⋃ ran ⁡ measures → dom ⁡ M ∈ ⋃ ran ⁡ sigAlgebra ∧ M : dom ⁡ M ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = ∑ * y ∈ x M ⁡ y
2 1 simprd ⊢ M ∈ ⋃ ran ⁡ measures → M : dom ⁡ M ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = ∑ * y ∈ x M ⁡ y
3 dmmeas ⊢ M ∈ ⋃ ran ⁡ measures → dom ⁡ M ∈ ⋃ ran ⁡ sigAlgebra
4 ismeas ⊢ dom ⁡ M ∈ ⋃ ran ⁡ sigAlgebra → M ∈ measures ⁡ dom ⁡ M ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = ∑ * y ∈ x M ⁡ y
5 3 4 syl ⊢ M ∈ ⋃ ran ⁡ measures → M ∈ measures ⁡ dom ⁡ M ↔ M : dom ⁡ M ⟶ 0 +∞ ∧ M ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 dom ⁡ M x ≼ ω ∧ Disj y ∈ x y → M ⁡ ⋃ x = ∑ * y ∈ x M ⁡ y
6 2 5 mpbird ⊢ M ∈ ⋃ ran ⁡ measures → M ∈ measures ⁡ dom ⁡ M
7 elfvunirn ⊢ M ∈ measures ⁡ dom ⁡ M → M ∈ ⋃ ran ⁡ measures
8 6 7 impbii ⊢ M ∈ ⋃ ran ⁡ measures ↔ M ∈ measures ⁡ dom ⁡ M