Metamath Proof Explorer


Theorem measssd

Description: A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016)

Ref Expression
Hypotheses measssd.1 φMmeasuresS
measssd.2 φAS
measssd.3 φBS
measssd.4 φAB
Assertion measssd φMAMB

Proof

Step Hyp Ref Expression
1 measssd.1 φMmeasuresS
2 measssd.2 φAS
3 measssd.3 φBS
4 measssd.4 φAB
5 measbase MmeasuresSSransigAlgebra
6 1 5 syl φSransigAlgebra
7 difelsiga SransigAlgebraBSASBAS
8 6 3 2 7 syl3anc φBAS
9 measvxrge0 MmeasuresSBASMBA0+∞
10 1 8 9 syl2anc φMBA0+∞
11 elxrge0 MBA0+∞MBA*0MBA
12 11 simprbi MBA0+∞0MBA
13 10 12 syl φ0MBA
14 measvxrge0 MmeasuresSASMA0+∞
15 1 2 14 syl2anc φMA0+∞
16 elxrge0 MA0+∞MA*0MA
17 16 simplbi MA0+∞MA*
18 15 17 syl φMA*
19 11 simplbi MBA0+∞MBA*
20 10 19 syl φMBA*
21 xraddge02 MA*MBA*0MBAMAMA+𝑒MBA
22 18 20 21 syl2anc φ0MBAMAMA+𝑒MBA
23 13 22 mpd φMAMA+𝑒MBA
24 prssi ASBASABAS
25 2 8 24 syl2anc φABAS
26 prex ABAV
27 26 elpw ABA𝒫SABAS
28 25 27 sylibr φABA𝒫S
29 prct ASBASABAω
30 2 8 29 syl2anc φABAω
31 disjdifprg ASBSDisjyBAAy
32 2 3 31 syl2anc φDisjyBAAy
33 prcom BAA=ABA
34 33 a1i φBAA=ABA
35 34 disjeq1d φDisjyBAAyDisjyABAy
36 32 35 mpbid φDisjyABAy
37 measvun MmeasuresSABA𝒫SABAωDisjyABAyMABA=*yABAMy
38 1 28 30 36 37 syl112anc φMABA=*yABAMy
39 uniprg ASBASABA=ABA
40 2 8 39 syl2anc φABA=ABA
41 undif ABABA=B
42 4 41 sylib φABA=B
43 40 42 eqtrd φABA=B
44 43 fveq2d φMABA=MB
45 fveq2 y=AMy=MA
46 45 adantl φy=AMy=MA
47 fveq2 y=BAMy=MBA
48 47 adantl φy=BAMy=MBA
49 eqimss A=BAABA
50 ssdifeq0 ABAA=
51 49 50 sylib A=BAA=
52 51 adantl φA=BAA=
53 52 fveq2d φA=BAMA=M
54 measvnul MmeasuresSM=0
55 1 54 syl φM=0
56 55 adantr φA=BAM=0
57 53 56 eqtrd φA=BAMA=0
58 57 orcd φA=BAMA=0MA=+∞
59 58 ex φA=BAMA=0MA=+∞
60 46 48 2 8 15 10 59 esumpr2 φ*yABAMy=MA+𝑒MBA
61 38 44 60 3eqtr3d φMB=MA+𝑒MBA
62 23 61 breqtrrd φMAMB