Description: A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | measssd.1 | |
|
measssd.2 | |
||
measssd.3 | |
||
measssd.4 | |
||
Assertion | measssd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | measssd.1 | |
|
2 | measssd.2 | |
|
3 | measssd.3 | |
|
4 | measssd.4 | |
|
5 | measbase | |
|
6 | 1 5 | syl | |
7 | difelsiga | |
|
8 | 6 3 2 7 | syl3anc | |
9 | measvxrge0 | |
|
10 | 1 8 9 | syl2anc | |
11 | elxrge0 | |
|
12 | 11 | simprbi | |
13 | 10 12 | syl | |
14 | measvxrge0 | |
|
15 | 1 2 14 | syl2anc | |
16 | elxrge0 | |
|
17 | 16 | simplbi | |
18 | 15 17 | syl | |
19 | 11 | simplbi | |
20 | 10 19 | syl | |
21 | xraddge02 | |
|
22 | 18 20 21 | syl2anc | |
23 | 13 22 | mpd | |
24 | prssi | |
|
25 | 2 8 24 | syl2anc | |
26 | prex | |
|
27 | 26 | elpw | |
28 | 25 27 | sylibr | |
29 | prct | |
|
30 | 2 8 29 | syl2anc | |
31 | disjdifprg | |
|
32 | 2 3 31 | syl2anc | |
33 | prcom | |
|
34 | 33 | a1i | |
35 | 34 | disjeq1d | |
36 | 32 35 | mpbid | |
37 | measvun | |
|
38 | 1 28 30 36 37 | syl112anc | |
39 | uniprg | |
|
40 | 2 8 39 | syl2anc | |
41 | undif | |
|
42 | 4 41 | sylib | |
43 | 40 42 | eqtrd | |
44 | 43 | fveq2d | |
45 | fveq2 | |
|
46 | 45 | adantl | |
47 | fveq2 | |
|
48 | 47 | adantl | |
49 | eqimss | |
|
50 | ssdifeq0 | |
|
51 | 49 50 | sylib | |
52 | 51 | adantl | |
53 | 52 | fveq2d | |
54 | measvnul | |
|
55 | 1 54 | syl | |
56 | 55 | adantr | |
57 | 53 56 | eqtrd | |
58 | 57 | orcd | |
59 | 58 | ex | |
60 | 46 48 2 8 15 10 59 | esumpr2 | |
61 | 38 44 60 | 3eqtr3d | |
62 | 23 61 | breqtrrd | |