Description: The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | cntmeas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hashf2 | |
|
2 | ssv | |
|
3 | fssres | |
|
4 | 1 2 3 | mp2an | |
5 | 4 | a1i | |
6 | 0elsiga | |
|
7 | fvres | |
|
8 | 6 7 | syl | |
9 | hash0 | |
|
10 | 8 9 | eqtrdi | |
11 | vex | |
|
12 | hasheuni | |
|
13 | 11 12 | mpan | |
14 | 13 | ad2antll | |
15 | isrnsigau | |
|
16 | 15 | simprd | |
17 | 16 | simp3d | |
18 | fvres | |
|
19 | 18 | imim2i | |
20 | 19 | ralimi | |
21 | 17 20 | syl | |
22 | 21 | r19.21bi | |
23 | 22 | imp | |
24 | 23 | adantrr | |
25 | elpwi | |
|
26 | 25 | sseld | |
27 | fvres | |
|
28 | 26 27 | syl6 | |
29 | 28 | imp | |
30 | 29 | esumeq2dv | |
31 | 30 | ad2antlr | |
32 | 14 24 31 | 3eqtr4d | |
33 | 32 | ex | |
34 | 33 | ralrimiva | |
35 | ismeas | |
|
36 | 5 10 34 35 | mpbir3and | |