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		df-meas	⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
8	7	funmpt2	⊢ Fun measures
9		elunirn2	⊢ ( ( Fun measures ∧ 𝑀 ∈ ( measures ‘ dom 𝑀 ) ) → 𝑀 ∈ ∪ ran measures )
10	8 9	mpan	⊢ ( 𝑀 ∈ ( measures ‘ dom 𝑀 ) → 𝑀 ∈ ∪ ran measures )
11	6 10	impbii	⊢ ( 𝑀 ∈ ∪ ran measures ↔ 𝑀 ∈ ( measures ‘ dom 𝑀 ) )