Description: A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | measunl.1 | |
|
measunl.2 | |
||
measunl.3 | |
||
Assertion | measunl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | measunl.1 | |
|
2 | measunl.2 | |
|
3 | measunl.3 | |
|
4 | undif1 | |
|
5 | 4 | fveq2i | |
6 | measbase | |
|
7 | 1 6 | syl | |
8 | difelsiga | |
|
9 | 7 2 3 8 | syl3anc | |
10 | disjdifr | |
|
11 | 10 | a1i | |
12 | measun | |
|
13 | 1 9 3 11 12 | syl121anc | |
14 | 5 13 | eqtr3id | |
15 | iccssxr | |
|
16 | measvxrge0 | |
|
17 | 1 9 16 | syl2anc | |
18 | 15 17 | sselid | |
19 | measvxrge0 | |
|
20 | 1 2 19 | syl2anc | |
21 | 15 20 | sselid | |
22 | measvxrge0 | |
|
23 | 1 3 22 | syl2anc | |
24 | 15 23 | sselid | |
25 | inelsiga | |
|
26 | 7 2 3 25 | syl3anc | |
27 | measvxrge0 | |
|
28 | 1 26 27 | syl2anc | |
29 | elxrge0 | |
|
30 | 28 29 | sylib | |
31 | 30 | simprd | |
32 | 15 28 | sselid | |
33 | xraddge02 | |
|
34 | 18 32 33 | syl2anc | |
35 | 31 34 | mpd | |
36 | uncom | |
|
37 | inundif | |
|
38 | 36 37 | eqtr3i | |
39 | 38 | fveq2i | |
40 | incom | |
|
41 | inindif | |
|
42 | 40 41 | eqtr3i | |
43 | 42 | a1i | |
44 | measun | |
|
45 | 1 9 26 43 44 | syl121anc | |
46 | 39 45 | eqtr3id | |
47 | 35 46 | breqtrrd | |
48 | xleadd1a | |
|
49 | 18 21 24 47 48 | syl31anc | |
50 | 14 49 | eqbrtrd | |