Theorem measval

Description: The value of the measures function applied on a sigma-algebra. (Contributed by Thierry Arnoux, 17-Oct-2016)

	Ref	Expression
Assertion	measval	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( measures ‘ 𝑆 ) = { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) → 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) )
2	1	ss2abi	⊢ { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ⊆ { 𝑚 ∣ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) }
3		ovex	⊢ ( 0 [,] +∞ ) ∈ V
4		mapex	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( 0 [,] +∞ ) ∈ V ) → { 𝑚 ∣ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) } ∈ V )
5	3 4	mpan2	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → { 𝑚 ∣ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) } ∈ V )
6		ssexg	⊢ ( ( { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ⊆ { 𝑚 ∣ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) } ∧ { 𝑚 ∣ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) } ∈ V ) → { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ∈ V )
7	2 5 6	sylancr	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ∈ V )
8		feq2	⊢ ( 𝑠 = 𝑆 → ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ↔ 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ) )
9		pweq	⊢ ( 𝑠 = 𝑆 → 𝒫 𝑠 = 𝒫 𝑆 )
10	9	raleqdv	⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) )
11	8 10	3anbi13d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) ↔ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) ) )
12	11	abbidv	⊢ ( 𝑠 = 𝑆 → { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } = { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
13		df-meas	⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
14	12 13	fvmptg	⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ∈ V ) → ( measures ‘ 𝑆 ) = { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
15	7 14	mpdan	⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( measures ‘ 𝑆 ) = { 𝑚 ∣ ( 𝑚 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )