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 df-meas ⊢ measures = s ∈ ⋃ ran ⁡ sigAlgebra ⟼ m | m : s ⟶ 0 +∞ ∧ m ⁡ ∅ = 0 ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → m ⁡ ⋃ x = ∑ * y ∈ x m ⁡ y
8 7 funmpt2 ⊢ Fun ⁡ measures
9 elunirn2 ⊢ Fun ⁡ measures ∧ M ∈ measures ⁡ dom ⁡ M → M ∈ ⋃ ran ⁡ measures
10 8 9 mpan ⊢ M ∈ measures ⁡ dom ⁡ M → M ∈ ⋃ ran ⁡ measures
11 6 10 impbii ⊢ M ∈ ⋃ ran ⁡ measures ↔ M ∈ measures ⁡ dom ⁡ M