Metamath Proof Explorer


Theorem measunl

Description: A measure is sub-additive with respect to union. (Contributed by Thierry Arnoux, 20-Oct-2017)

Ref Expression
Hypotheses measunl.1 φMmeasuresS
measunl.2 φAS
measunl.3 φBS
Assertion measunl φMABMA+𝑒MB

Proof

Step Hyp Ref Expression
1 measunl.1 φMmeasuresS
2 measunl.2 φAS
3 measunl.3 φBS
4 undif1 ABB=AB
5 4 fveq2i MABB=MAB
6 measbase MmeasuresSSransigAlgebra
7 1 6 syl φSransigAlgebra
8 difelsiga SransigAlgebraASBSABS
9 7 2 3 8 syl3anc φABS
10 disjdifr ABB=
11 10 a1i φABB=
12 measun MmeasuresSABSBSABB=MABB=MAB+𝑒MB
13 1 9 3 11 12 syl121anc φMABB=MAB+𝑒MB
14 5 13 eqtr3id φMAB=MAB+𝑒MB
15 iccssxr 0+∞*
16 measvxrge0 MmeasuresSABSMAB0+∞
17 1 9 16 syl2anc φMAB0+∞
18 15 17 sselid φMAB*
19 measvxrge0 MmeasuresSASMA0+∞
20 1 2 19 syl2anc φMA0+∞
21 15 20 sselid φMA*
22 measvxrge0 MmeasuresSBSMB0+∞
23 1 3 22 syl2anc φMB0+∞
24 15 23 sselid φMB*
25 inelsiga SransigAlgebraASBSABS
26 7 2 3 25 syl3anc φABS
27 measvxrge0 MmeasuresSABSMAB0+∞
28 1 26 27 syl2anc φMAB0+∞
29 elxrge0 MAB0+∞MAB*0MAB
30 28 29 sylib φMAB*0MAB
31 30 simprd φ0MAB
32 15 28 sselid φMAB*
33 xraddge02 MAB*MAB*0MABMABMAB+𝑒MAB
34 18 32 33 syl2anc φ0MABMABMAB+𝑒MAB
35 31 34 mpd φMABMAB+𝑒MAB
36 uncom ABAB=ABAB
37 inundif ABAB=A
38 36 37 eqtr3i ABAB=A
39 38 fveq2i MABAB=MA
40 incom ABAB=ABAB
41 inindif ABAB=
42 40 41 eqtr3i ABAB=
43 42 a1i φABAB=
44 measun MmeasuresSABSABSABAB=MABAB=MAB+𝑒MAB
45 1 9 26 43 44 syl121anc φMABAB=MAB+𝑒MAB
46 39 45 eqtr3id φMA=MAB+𝑒MAB
47 35 46 breqtrrd φMABMA
48 xleadd1a MAB*MA*MB*MABMAMAB+𝑒MBMA+𝑒MB
49 18 21 24 47 48 syl31anc φMAB+𝑒MBMA+𝑒MB
50 14 49 eqbrtrd φMABMA+𝑒MB