Metamath Proof Explorer

Theorem ismea

Description: Express the predicate " M is a measure." Definition 112A of Fremlin1 p. 14. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion ismea ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 id ⊢ ( 𝑀 ∈ Meas → 𝑀 ∈ Meas )
2 fex ⊢ ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) → 𝑀 ∈ V )
3 id ⊢ ( 𝑧 = 𝑀 → 𝑧 = 𝑀 )
4 dmeq ⊢ ( 𝑧 = 𝑀 → dom 𝑧 = dom 𝑀 )
5 3 4 feq12d ⊢ ( 𝑧 = 𝑀 → ( 𝑧 : dom 𝑧 ⟶ ( 0 [,] +∞ ) ↔ 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ) )
6 4 eleq1d ⊢ ( 𝑧 = 𝑀 → ( dom 𝑧 ∈ SAlg ↔ dom 𝑀 ∈ SAlg ) )
7 5 6 anbi12d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑧 : dom 𝑧 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑧 ∈ SAlg ) ↔ ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ) )
8 fveq1 ⊢ ( 𝑧 = 𝑀 → ( 𝑧 ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
9 8 eqeq1d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑧 ‘ ∅ ) = 0 ↔ ( 𝑀 ‘ ∅ ) = 0 ) )
10 7 9 anbi12d ⊢ ( 𝑧 = 𝑀 → ( ( ( 𝑧 : dom 𝑧 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑧 ∈ SAlg ) ∧ ( 𝑧 ‘ ∅ ) = 0 ) ↔ ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ) )
11 4 pweqd ⊢ ( 𝑧 = 𝑀 → 𝒫 dom 𝑧 = 𝒫 dom 𝑀 )
12 fveq1 ⊢ ( 𝑧 = 𝑀 → ( 𝑧 ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑥 ) )
13 reseq1 ⊢ ( 𝑧 = 𝑀 → ( 𝑧 ↾ 𝑥 ) = ( 𝑀 ↾ 𝑥 ) )
14 13 fveq2d ⊢ ( 𝑧 = 𝑀 → ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) )
15 12 14 eqeq12d ⊢ ( 𝑧 = 𝑀 → ( ( 𝑧 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) ↔ ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) )
16 15 imbi2d ⊢ ( 𝑧 = 𝑀 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑧 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) ) ↔ ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
17 11 16 raleqbidv ⊢ ( 𝑧 = 𝑀 → ( ∀ 𝑥 ∈ 𝒫 dom 𝑧 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑧 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )
18 10 17 anbi12d ⊢ ( 𝑧 = 𝑀 → ( ( ( ( 𝑧 : dom 𝑧 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑧 ∈ SAlg ) ∧ ( 𝑧 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑧 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑧 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) ) ) ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) ) )
19 df-mea ⊢ Meas = { 𝑧 ∣ ( ( ( 𝑧 : dom 𝑧 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑧 ∈ SAlg ) ∧ ( 𝑧 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑧 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑧 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑧 ↾ 𝑥 ) ) ) ) }
20 18 19 elab2g ⊢ ( 𝑀 ∈ V → ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) ) )
21 2 20 syl ⊢ ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) → ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) ) )
22 21 ad2antrr ⊢ ( ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) → ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) ) )
23 22 ibir ⊢ ( ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) → 𝑀 ∈ Meas )
24 18 19 elab2g ⊢ ( 𝑀 ∈ Meas → ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) ) )
25 1 23 24 pm5.21nii ⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑥 ∈ 𝒫 dom 𝑀 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( 𝑀 ‘ ∪ 𝑥 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑥 ) ) ) ) )