Metamath Proof Explorer


Theorem omeunle

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 φOOutMeas
omeunle.x X=domO
omeunle.a φAX
omeunle.b φBX
Assertion omeunle φOABOA+𝑒OB

Proof

Step Hyp Ref Expression
1 omeunle.o φOOutMeas
2 omeunle.x X=domO
3 omeunle.a φAX
4 omeunle.b φBX
5 1 2 unidmex φXV
6 ssexg AXXVAV
7 3 5 6 syl2anc φAV
8 ssexg BXXVBV
9 4 5 8 syl2anc φBV
10 uniprg AVBVAB=AB
11 7 9 10 syl2anc φAB=AB
12 11 eqcomd φAB=AB
13 12 fveq2d φOAB=OAB
14 iccssxr 0+∞*
15 3 4 unssd φABX
16 11 15 eqsstrd φABX
17 1 2 16 omecl φOAB0+∞
18 14 17 sselid φOAB*
19 prfi ABFin
20 19 elexi ABV
21 20 a1i φABV
22 1 2 omef φO:𝒫X0+∞
23 elpwg AVA𝒫XAX
24 7 23 syl φA𝒫XAX
25 3 24 mpbird φA𝒫X
26 elpwg BVB𝒫XBX
27 9 26 syl φB𝒫XBX
28 4 27 mpbird φB𝒫X
29 25 28 jca φA𝒫XB𝒫X
30 prssg AVBVA𝒫XB𝒫XAB𝒫X
31 7 9 30 syl2anc φA𝒫XB𝒫XAB𝒫X
32 29 31 mpbid φAB𝒫X
33 22 32 fssresd φOAB:AB0+∞
34 21 33 sge0xrcl φsum^OAB*
35 1 2 3 omecl φOA0+∞
36 14 35 sselid φOA*
37 1 2 4 omecl φOB0+∞
38 14 37 sselid φOB*
39 36 38 xaddcld φOA+𝑒OB*
40 isfinite ABFinABω
41 40 biimpi ABFinABω
42 sdomdom ABωABω
43 41 42 syl ABFinABω
44 19 43 ax-mp ABω
45 44 a1i φABω
46 1 2 32 45 omeunile φOABsum^OAB
47 22 32 feqresmpt φOAB=kABOk
48 47 fveq2d φsum^OAB=sum^kABOk
49 fveq2 k=AOk=OA
50 fveq2 k=BOk=OB
51 7 9 35 37 49 50 sge0prle φsum^kABOkOA+𝑒OB
52 48 51 eqbrtrd φsum^OABOA+𝑒OB
53 18 34 39 46 52 xrletrd φOABOA+𝑒OB
54 13 53 eqbrtrd φOABOA+𝑒OB