Description: The outer measure of the union of two sets is less than or equal to the sum of the measures, Remark 113B (c) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | omeunle.o | |
|
omeunle.x | |
||
omeunle.a | |
||
omeunle.b | |
||
Assertion | omeunle | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | omeunle.o | |
|
2 | omeunle.x | |
|
3 | omeunle.a | |
|
4 | omeunle.b | |
|
5 | 1 2 | unidmex | |
6 | ssexg | |
|
7 | 3 5 6 | syl2anc | |
8 | ssexg | |
|
9 | 4 5 8 | syl2anc | |
10 | uniprg | |
|
11 | 7 9 10 | syl2anc | |
12 | 11 | eqcomd | |
13 | 12 | fveq2d | |
14 | iccssxr | |
|
15 | 3 4 | unssd | |
16 | 11 15 | eqsstrd | |
17 | 1 2 16 | omecl | |
18 | 14 17 | sselid | |
19 | prfi | |
|
20 | 19 | elexi | |
21 | 20 | a1i | |
22 | 1 2 | omef | |
23 | elpwg | |
|
24 | 7 23 | syl | |
25 | 3 24 | mpbird | |
26 | elpwg | |
|
27 | 9 26 | syl | |
28 | 4 27 | mpbird | |
29 | 25 28 | jca | |
30 | prssg | |
|
31 | 7 9 30 | syl2anc | |
32 | 29 31 | mpbid | |
33 | 22 32 | fssresd | |
34 | 21 33 | sge0xrcl | |
35 | 1 2 3 | omecl | |
36 | 14 35 | sselid | |
37 | 1 2 4 | omecl | |
38 | 14 37 | sselid | |
39 | 36 38 | xaddcld | |
40 | isfinite | |
|
41 | 40 | biimpi | |
42 | sdomdom | |
|
43 | 41 42 | syl | |
44 | 19 43 | ax-mp | |
45 | 44 | a1i | |
46 | 1 2 32 45 | omeunile | |
47 | 22 32 | feqresmpt | |
48 | 47 | fveq2d | |
49 | fveq2 | |
|
50 | fveq2 | |
|
51 | 7 9 35 37 49 50 | sge0prle | |
52 | 48 51 | eqbrtrd | |
53 | 18 34 39 46 52 | xrletrd | |
54 | 13 53 | eqbrtrd | |