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 ≤ ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑀 ‘ 𝐴 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) )
22	18 20 21	syl2anc	⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑀 ‘ 𝐴 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) ) )
23	13 22	mpd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
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	⊢ ( 𝜑 → Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑀 ‘ 𝑦 ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
61	38 44 60	3eqtr3d	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( ( 𝑀 ‘ 𝐴 ) +e ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
62	23 61	breqtrrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )