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 SransigAlgebra.SmeasuresS

Proof

Step Hyp Ref Expression
1 hashf2 .:V0+∞
2 ssv SV
3 fssres .:V0+∞SV.S:S0+∞
4 1 2 3 mp2an .S:S0+∞
5 4 a1i SransigAlgebra.S:S0+∞
6 0elsiga SransigAlgebraS
7 fvres S.S=
8 6 7 syl SransigAlgebra.S=
9 hash0 =0
10 8 9 eqtrdi SransigAlgebra.S=0
11 vex xV
12 hasheuni xVDisjyxyx=*yxy
13 11 12 mpan Disjyxyx=*yxy
14 13 ad2antll SransigAlgebrax𝒫SxωDisjyxyx=*yxy
15 isrnsigau SransigAlgebraS𝒫SSSxSSxSx𝒫SxωxS
16 15 simprd SransigAlgebraSSxSSxSx𝒫SxωxS
17 16 simp3d SransigAlgebrax𝒫SxωxS
18 fvres xS.Sx=x
19 18 imim2i xωxSxω.Sx=x
20 19 ralimi x𝒫SxωxSx𝒫Sxω.Sx=x
21 17 20 syl SransigAlgebrax𝒫Sxω.Sx=x
22 21 r19.21bi SransigAlgebrax𝒫Sxω.Sx=x
23 22 imp SransigAlgebrax𝒫Sxω.Sx=x
24 23 adantrr SransigAlgebrax𝒫SxωDisjyxy.Sx=x
25 elpwi x𝒫SxS
26 25 sseld x𝒫SyxyS
27 fvres yS.Sy=y
28 26 27 syl6 x𝒫Syx.Sy=y
29 28 imp x𝒫Syx.Sy=y
30 29 esumeq2dv x𝒫S*yx.Sy=*yxy
31 30 ad2antlr SransigAlgebrax𝒫SxωDisjyxy*yx.Sy=*yxy
32 14 24 31 3eqtr4d SransigAlgebrax𝒫SxωDisjyxy.Sx=*yx.Sy
33 32 ex SransigAlgebrax𝒫SxωDisjyxy.Sx=*yx.Sy
34 33 ralrimiva SransigAlgebrax𝒫SxωDisjyxy.Sx=*yx.Sy
35 ismeas SransigAlgebra.SmeasuresS.S:S0+∞.S=0x𝒫SxωDisjyxy.Sx=*yx.Sy
36 5 10 34 35 mpbir3and SransigAlgebra.SmeasuresS