Description: The measure of the disjoint union of a countable set is the extended sum of the measures. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | meadjiun.1 | |
|
meadjiun.m | |
||
meadjiun.s | |
||
meadjiun.b | |
||
meadjiun.a | |
||
meadjiun.dj | |
||
Assertion | meadjiun | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | meadjiun.1 | |
|
2 | meadjiun.m | |
|
3 | meadjiun.s | |
|
4 | meadjiun.b | |
|
5 | meadjiun.a | |
|
6 | meadjiun.dj | |
|
7 | 4 | ex | |
8 | 1 7 | ralrimi | |
9 | dfiun3g | |
|
10 | 8 9 | syl | |
11 | 10 | fveq2d | |
12 | eqid | |
|
13 | 1 12 4 | rnmptssd | |
14 | 1stcrestlem | |
|
15 | 5 14 | syl | |
16 | 12 | disjrnmpt2 | |
17 | 6 16 | syl | |
18 | 2 3 13 15 17 | meadjuni | |
19 | reldom | |
|
20 | brrelex1 | |
|
21 | 19 20 | mpan | |
22 | 5 21 | syl | |
23 | 1 4 12 | fmptdf | |
24 | fveq2 | |
|
25 | 24 | neeq1d | |
26 | 25 | cbvrabv | |
27 | simpr | |
|
28 | nfv | |
|
29 | 1 28 | nfan | |
30 | nfcv | |
|
31 | 30 | nfcsb1 | |
32 | nfcv | |
|
33 | 31 32 | nfel | |
34 | 29 33 | nfim | |
35 | eleq1w | |
|
36 | 35 | anbi2d | |
37 | csbeq1a | |
|
38 | 37 | eleq1d | |
39 | 36 38 | imbi12d | |
40 | 34 39 4 | chvarfv | |
41 | 30 31 37 12 | fvmptf | |
42 | 27 40 41 | syl2anc | |
43 | 42 | disjeq2dv | |
44 | nfcv | |
|
45 | 44 31 37 | cbvdisj | |
46 | 45 | bicomi | |
47 | 46 | a1i | |
48 | 43 47 | bitrd | |
49 | 6 48 | mpbird | |
50 | 2 3 22 23 26 49 | meadjiunlem | |
51 | 44 31 37 | cbvmpt | |
52 | 51 | coeq2i | |
53 | 52 | a1i | |
54 | eqidd | |
|
55 | 2 3 | meaf | |
56 | 55 | feqmptd | |
57 | fveq2 | |
|
58 | 40 54 56 57 | fmptco | |
59 | nfcv | |
|
60 | nfcv | |
|
61 | 60 31 | nffv | |
62 | 37 | fveq2d | |
63 | 59 61 62 | cbvmpt | |
64 | 63 | eqcomi | |
65 | 64 | a1i | |
66 | 53 58 65 | 3eqtrd | |
67 | 66 | fveq2d | |
68 | 50 67 | eqtrd | |
69 | 11 18 68 | 3eqtrd | |