Metamath Proof Explorer

Theorem cntmeas

Description: The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion cntmeas ( 𝑆 ∈ ∪ ran sigAlgebra → ( ♯ ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 hashf2 ⊢ ♯ : V ⟶ ( 0 [,] +∞ )
2 ssv ⊢ 𝑆 ⊆ V
3 fssres ⊢ ( ( ♯ : V ⟶ ( 0 [,] +∞ ) ∧ 𝑆 ⊆ V ) → ( ♯ ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
4 1 2 3 mp2an ⊢ ( ♯ ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ )
5 4 a1i ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ♯ ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) )
6 0elsiga ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑆 )
7 fvres ⊢ ( ∅ ∈ 𝑆 → ( ( ♯ ↾ 𝑆 ) ‘ ∅ ) = ( ♯ ‘ ∅ ) )
8 6 7 syl ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( ♯ ↾ 𝑆 ) ‘ ∅ ) = ( ♯ ‘ ∅ ) )
9 hash0 ⊢ ( ♯ ‘ ∅ ) = 0
10 8 9 eqtrdi ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( ♯ ↾ 𝑆 ) ‘ ∅ ) = 0 )
11 vex ⊢ 𝑥 ∈ V
12 hasheuni ⊢ ( ( 𝑥 ∈ V ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ♯ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ♯ ‘ 𝑦 ) )
13 11 12 mpan ⊢ ( Disj 𝑦 ∈ 𝑥 𝑦 → ( ♯ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ♯ ‘ 𝑦 ) )
14 13 ad2antll ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ♯ ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ♯ ‘ 𝑦 ) )
15 isrnsigau ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( 𝑆 ⊆ 𝒫 ∪ 𝑆 ∧ ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) ) )
16 15 simprd ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ∪ 𝑆 ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( ∪ 𝑆 ∖ 𝑥 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) ) )
17 16 simp3d ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) )
18 fvres ⊢ ( ∪ 𝑥 ∈ 𝑆 → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) )
19 18 imim2i ⊢ ( ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ( 𝑥 ≼ ω → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) ) )
20 19 ralimi ⊢ ( ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑆 ) → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) ) )
21 17 20 syl ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( 𝑥 ≼ ω → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) ) )
22 21 r19.21bi ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) → ( 𝑥 ≼ ω → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) ) )
23 22 imp ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ 𝑥 ≼ ω ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) )
24 23 adantrr ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = ( ♯ ‘ ∪ 𝑥 ) )
25 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑆 → 𝑥 ⊆ 𝑆 )
26 25 sseld ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ( 𝑦 ∈ 𝑥 → 𝑦 ∈ 𝑆 ) )
27 fvres ⊢ ( 𝑦 ∈ 𝑆 → ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) = ( ♯ ‘ 𝑦 ) )
28 26 27 syl6 ⊢ ( 𝑥 ∈ 𝒫 𝑆 → ( 𝑦 ∈ 𝑥 → ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) = ( ♯ ‘ 𝑦 ) ) )
29 28 imp ⊢ ( ( 𝑥 ∈ 𝒫 𝑆 ∧ 𝑦 ∈ 𝑥 ) → ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) = ( ♯ ‘ 𝑦 ) )
30 29 esumeq2dv ⊢ ( 𝑥 ∈ 𝒫 𝑆 → Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( ♯ ‘ 𝑦 ) )
31 30 ad2antlr ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( ♯ ‘ 𝑦 ) )
32 14 24 31 3eqtr4d ⊢ ( ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) )
33 32 ex ⊢ ( ( 𝑆 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑆 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) ) )
34 33 ralrimiva ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) ) )
35 ismeas ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ( ♯ ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) ↔ ( ( ♯ ↾ 𝑆 ) : 𝑆 ⟶ ( 0 [,] +∞ ) ∧ ( ( ♯ ↾ 𝑆 ) ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑆 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( ♯ ↾ 𝑆 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( ♯ ↾ 𝑆 ) ‘ 𝑦 ) ) ) ) )
36 5 10 34 35 mpbir3and ⊢ ( 𝑆 ∈ ∪ ran sigAlgebra → ( ♯ ↾ 𝑆 ) ∈ ( measures ‘ 𝑆 ) )