Metamath Proof Explorer

Theorem ismeas

Description: The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016) (Revised by Thierry Arnoux, 19-Oct-2016)

Ref Expression
Assertion ismeas ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 ∈ V )
2 1 a1i ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 ∈ V ) )
3 simp1 ⊢ ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
4 ovex ⊢ ( 0 [,] +∞ ) ∈ V
5 fex2 ⊢ ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ 𝑆 ∈ ∪ ran sigAlgebra ∧ ( 0 [,] +∞ ) ∈ V ) → 𝑀 ∈ V )
6 5 3expb ⊢ ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( 0 [,] +∞ ) ∈ V ) ) → 𝑀 ∈ V )
7 6 expcom ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ ( 0 [,] +∞ ) ∈ V ) → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) → 𝑀 ∈ V ) )
8 4 7 mpan2 ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) → 𝑀 ∈ V ) )
9 3 8 syl5 ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) → 𝑀 ∈ V ) )
10 df-meas ⊢ measures = ( 𝑠 ∈ ∪ ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } )
11 vex ⊢ 𝑠 ∈ V
12 mapex ⊢ ( ( 𝑠 ∈ V ∧ ( 0 [,] +∞ ) ∈ V ) → { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V )
13 11 4 12 mp2an ⊢ { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) } ∈ V
14 simp1 ⊢ ( ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) → 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) )
15 14 ss2abi ⊢ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ⊆ { 𝑚 ∣ 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) }
16 13 15 ssexi ⊢ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) } ∈ V
17 simpr ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝑚 = 𝑀 )
18 simpl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝑠 = 𝑆 )
19 17 18 feq12d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ↔ 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ) )
20 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
21 20 eqeq1d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ∅ ) = 0 ↔ ( 𝑀 ‘ ∅ ) = 0 ) )
22 21 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 ‘ ∅ ) = 0 ↔ ( 𝑀 ‘ ∅ ) = 0 ) )
23 18 pweqd ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → 𝒫 𝑠 = 𝒫 𝑆 )
24 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑥 ) )
25 fveq1 ⊢ ( 𝑚 = 𝑀 → ( 𝑚 ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) )
26 25 esumeq2sdv ⊢ ( 𝑚 = 𝑀 → Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
27 24 26 eqeq12d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ↔ ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) )
28 27 imbi2d ⊢ ( 𝑚 = 𝑀 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) )
29 28 adantl ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ↔ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) )
30 23 29 raleqbidv ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) )
31 19 22 30 3anbi123d ⊢ ( ( 𝑠 = 𝑆 ∧ 𝑚 = 𝑀 ) → ( ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑚 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑚 ‘ 𝑦 ) ) ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) )
32 10 16 31 abfmpel ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑀 ∈ V ) → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) )
33 32 ex ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ V → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) ) )
34 2 9 33 pm5.21ndd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑀 ∈ ( measures ‘ 𝑆 ) ↔ ( 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑀 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) ) ) ) )