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 ( 𝜑𝑀 ∈ ( measures ‘ 𝑆 ) )
measssd.2 ( 𝜑𝐴𝑆 )
measssd.3 ( 𝜑𝐵𝑆 )
measssd.4 ( 𝜑𝐴𝐵 )
Assertion measssd ( 𝜑 → ( 𝑀𝐴 ) ≤ ( 𝑀𝐵 ) )

Proof

Step Hyp Ref Expression
1 measssd.1 ( 𝜑𝑀 ∈ ( measures ‘ 𝑆 ) )
2 measssd.2 ( 𝜑𝐴𝑆 )
3 measssd.3 ( 𝜑𝐵𝑆 )
4 measssd.4 ( 𝜑𝐴𝐵 )
5 measbase ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ran sigAlgebra )
6 1 5 syl ( 𝜑𝑆 ran sigAlgebra )
7 difelsiga ( ( 𝑆 ran sigAlgebra ∧ 𝐵𝑆𝐴𝑆 ) → ( 𝐵𝐴 ) ∈ 𝑆 )
8 6 3 2 7 syl3anc ( 𝜑 → ( 𝐵𝐴 ) ∈ 𝑆 )
9 measvxrge0 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ ( 𝐵𝐴 ) ∈ 𝑆 ) → ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ( 0 [,] +∞ ) )
10 1 8 9 syl2anc ( 𝜑 → ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ( 0 [,] +∞ ) )
11 elxrge0 ( ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ℝ* ∧ 0 ≤ ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) )
12 11 simprbi ( ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑀 ‘ ( 𝐵𝐴 ) ) )
13 10 12 syl ( 𝜑 → 0 ≤ ( 𝑀 ‘ ( 𝐵𝐴 ) ) )
14 measvxrge0 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
15 1 2 14 syl2anc ( 𝜑 → ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) )
16 elxrge0 ( ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑀𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝑀𝐴 ) ) )
17 16 simplbi ( ( 𝑀𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝑀𝐴 ) ∈ ℝ* )
18 15 17 syl ( 𝜑 → ( 𝑀𝐴 ) ∈ ℝ* )
19 11 simplbi ( ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ( 0 [,] +∞ ) → ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ℝ* )
20 10 19 syl ( 𝜑 → ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ℝ* )
21 xraddge02 ( ( ( 𝑀𝐴 ) ∈ ℝ* ∧ ( 𝑀 ‘ ( 𝐵𝐴 ) ) ∈ ℝ* ) → ( 0 ≤ ( 𝑀 ‘ ( 𝐵𝐴 ) ) → ( 𝑀𝐴 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) ) )
22 18 20 21 syl2anc ( 𝜑 → ( 0 ≤ ( 𝑀 ‘ ( 𝐵𝐴 ) ) → ( 𝑀𝐴 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) ) )
23 13 22 mpd ( 𝜑 → ( 𝑀𝐴 ) ≤ ( ( 𝑀𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) )
24 prssi ( ( 𝐴𝑆 ∧ ( 𝐵𝐴 ) ∈ 𝑆 ) → { 𝐴 , ( 𝐵𝐴 ) } ⊆ 𝑆 )
25 2 8 24 syl2anc ( 𝜑 → { 𝐴 , ( 𝐵𝐴 ) } ⊆ 𝑆 )
26 prex { 𝐴 , ( 𝐵𝐴 ) } ∈ V
27 26 elpw ( { 𝐴 , ( 𝐵𝐴 ) } ∈ 𝒫 𝑆 ↔ { 𝐴 , ( 𝐵𝐴 ) } ⊆ 𝑆 )
28 25 27 sylibr ( 𝜑 → { 𝐴 , ( 𝐵𝐴 ) } ∈ 𝒫 𝑆 )
29 prct ( ( 𝐴𝑆 ∧ ( 𝐵𝐴 ) ∈ 𝑆 ) → { 𝐴 , ( 𝐵𝐴 ) } ≼ ω )
30 2 8 29 syl2anc ( 𝜑 → { 𝐴 , ( 𝐵𝐴 ) } ≼ ω )
31 disjdifprg ( ( 𝐴𝑆𝐵𝑆 ) → Disj 𝑦 ∈ { ( 𝐵𝐴 ) , 𝐴 } 𝑦 )
32 2 3 31 syl2anc ( 𝜑Disj 𝑦 ∈ { ( 𝐵𝐴 ) , 𝐴 } 𝑦 )
33 prcom { ( 𝐵𝐴 ) , 𝐴 } = { 𝐴 , ( 𝐵𝐴 ) }
34 33 a1i ( 𝜑 → { ( 𝐵𝐴 ) , 𝐴 } = { 𝐴 , ( 𝐵𝐴 ) } )
35 34 disjeq1d ( 𝜑 → ( Disj 𝑦 ∈ { ( 𝐵𝐴 ) , 𝐴 } 𝑦Disj 𝑦 ∈ { 𝐴 , ( 𝐵𝐴 ) } 𝑦 ) )
36 32 35 mpbid ( 𝜑Disj 𝑦 ∈ { 𝐴 , ( 𝐵𝐴 ) } 𝑦 )
37 measvun ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ { 𝐴 , ( 𝐵𝐴 ) } ∈ 𝒫 𝑆 ∧ ( { 𝐴 , ( 𝐵𝐴 ) } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵𝐴 ) } 𝑦 ) ) → ( 𝑀 { 𝐴 , ( 𝐵𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵𝐴 ) } ( 𝑀𝑦 ) )
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 ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )
55 1 54 syl ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
56 55 adantr ( ( 𝜑𝐴 = ( 𝐵𝐴 ) ) → ( 𝑀 ‘ ∅ ) = 0 )
57 53 56 eqtrd ( ( 𝜑𝐴 = ( 𝐵𝐴 ) ) → ( 𝑀𝐴 ) = 0 )
58 57 orcd ( ( 𝜑𝐴 = ( 𝐵𝐴 ) ) → ( ( 𝑀𝐴 ) = 0 ∨ ( 𝑀𝐴 ) = +∞ ) )
59 58 ex ( 𝜑 → ( 𝐴 = ( 𝐵𝐴 ) → ( ( 𝑀𝐴 ) = 0 ∨ ( 𝑀𝐴 ) = +∞ ) ) )
60 46 48 2 8 15 10 59 esumpr2 ( 𝜑 → Σ* 𝑦 ∈ { 𝐴 , ( 𝐵𝐴 ) } ( 𝑀𝑦 ) = ( ( 𝑀𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) )
61 38 44 60 3eqtr3d ( 𝜑 → ( 𝑀𝐵 ) = ( ( 𝑀𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵𝐴 ) ) ) )
62 23 61 breqtrrd ( 𝜑 → ( 𝑀𝐴 ) ≤ ( 𝑀𝐵 ) )