Metamath Proof Explorer

Theorem pmeasmono

Description: This theorem's hypotheses define a pre-measure. A pre-measure is monotone. (Contributed by Thierry Arnoux, 19-Jul-2020)

Ref Expression
Hypotheses caraext.1 ⊢ ( 𝜑 → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
caraext.2 ⊢ ( 𝜑 → ( 𝑃 ‘ ∅ ) = 0 )
caraext.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) )
pmeasmono.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
pmeasmono.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑅 )
pmeasmono.3 ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 )
pmeasmono.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion pmeasmono ( 𝜑 → ( 𝑃 ‘ 𝐴 ) ≤ ( 𝑃 ‘ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 caraext.1 ⊢ ( 𝜑 → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
2 caraext.2 ⊢ ( 𝜑 → ( 𝑃 ‘ ∅ ) = 0 )
3 caraext.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) )
4 pmeasmono.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
5 pmeasmono.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑅 )
6 pmeasmono.3 ⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 )
7 pmeasmono.4 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
8 eqimss ⊢ ( 𝐴 = ( 𝐵 ∖ 𝐴 ) → 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) )
9 ssdifeq0 ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐴 ) ↔ 𝐴 = ∅ )
10 8 9 sylib ⊢ ( 𝐴 = ( 𝐵 ∖ 𝐴 ) → 𝐴 = ∅ )
11 10 fveq2d ⊢ ( 𝐴 = ( 𝐵 ∖ 𝐴 ) → ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ∅ ) )
12 11 adantl ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ∅ ) )
13 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ ∅ ) = 0 )
14 12 13 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) = 0 )
15 1 5 ffvelrnd ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
16 elxrge0 ⊢ ( ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝑃 ‘ 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 ‘ 𝐵 ) ) )
17 16 simprbi ⊢ ( ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝑃 ‘ 𝐵 ) )
18 15 17 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑃 ‘ 𝐵 ) )
19 18 adantr ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝐵 ∖ 𝐴 ) ) → 0 ≤ ( 𝑃 ‘ 𝐵 ) )
20 14 19 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 = ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) ≤ ( 𝑃 ‘ 𝐵 ) )
21 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
22 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → 𝑃 : 𝑅 ⟶ ( 0 [,] +∞ ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → 𝐴 ∈ 𝑅 )
24 22 23 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
25 21 24 sselid ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) ∈ ℝ* )
26 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 )
27 22 26 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
28 xrge0addge ⊢ ( ( ( 𝑃 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) ) → ( 𝑃 ‘ 𝐴 ) ≤ ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
29 25 27 28 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) ≤ ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
30 prct ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 ) → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω )
31 4 6 30 syl2anc ⊢ ( 𝜑 → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω )
33 prssi ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 ) → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 )
34 4 6 33 syl2anc ⊢ ( 𝜑 → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 )
36 disjdif ⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
37 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) )
38 id ⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
39 id ⊢ ( 𝑦 = ( 𝐵 ∖ 𝐴 ) → 𝑦 = ( 𝐵 ∖ 𝐴 ) )
40 38 39 disjprg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ ) )
41 23 26 37 40 syl3anc ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ↔ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ ) )
42 36 41 mpbiri ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 )
43 32 35 42 3jca ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) )
44 prex ⊢ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ∈ V
45 biidd ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( 𝜑 ↔ 𝜑 ) )
46 breq1 ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( 𝑥 ≼ ω ↔ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ) )
47 sseq1 ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( 𝑥 ⊆ 𝑅 ↔ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ) )
48 disjeq1 ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) )
49 46 47 48 3anbi123d ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) )
50 45 49 anbi12d ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) ↔ ( 𝜑 ∧ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) ) )
51 unieq ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ∪ 𝑥 = ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } )
52 51 fveq2d ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( 𝑃 ‘ ∪ 𝑥 ) = ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) )
53 esumeq1 ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) )
54 52 53 eqeq12d ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) ↔ ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) ) )
55 50 54 imbi12d ⊢ ( 𝑥 = { 𝐴 , ( 𝐵 ∖ 𝐴 ) } → ( ( ( 𝜑 ∧ ( 𝑥 ≼ ω ∧ 𝑥 ⊆ 𝑅 ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑃 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑃 ‘ 𝑦 ) ) ↔ ( ( 𝜑 ∧ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) ) ) )
56 55 3 vtoclg ⊢ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ∈ V → ( ( 𝜑 ∧ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) ) )
57 44 56 ax-mp ⊢ ( ( 𝜑 ∧ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) )
58 57 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) ∧ ( { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ≼ ω ∧ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ⊆ 𝑅 ∧ Disj 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } 𝑦 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) )
59 43 58 mpdan ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) )
60 uniprg ⊢ ( ( 𝐴 ∈ 𝑅 ∧ ( 𝐵 ∖ 𝐴 ) ∈ 𝑅 ) → ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } = ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) )
61 4 6 60 syl2anc ⊢ ( 𝜑 → ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } = ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) )
62 undif ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
63 7 62 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
64 61 63 eqtrd ⊢ ( 𝜑 → ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } = 𝐵 )
65 64 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } = 𝐵 )
66 65 fveq2d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ ∪ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ) = ( 𝑃 ‘ 𝐵 ) )
67 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) ∧ 𝑦 = 𝐴 ) → 𝑦 = 𝐴 )
68 67 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) ∧ 𝑦 = 𝐴 ) → ( 𝑃 ‘ 𝑦 ) = ( 𝑃 ‘ 𝐴 ) )
69 simpr ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) ∧ 𝑦 = ( 𝐵 ∖ 𝐴 ) ) → 𝑦 = ( 𝐵 ∖ 𝐴 ) )
70 69 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) ∧ 𝑦 = ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝑦 ) = ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) )
71 68 70 23 26 24 27 37 esumpr ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → Σ* 𝑦 ∈ { 𝐴 , ( 𝐵 ∖ 𝐴 ) } ( 𝑃 ‘ 𝑦 ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
72 59 66 71 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐵 ) = ( ( 𝑃 ‘ 𝐴 ) +𝑒 ( 𝑃 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
73 29 72 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ≠ ( 𝐵 ∖ 𝐴 ) ) → ( 𝑃 ‘ 𝐴 ) ≤ ( 𝑃 ‘ 𝐵 ) )
74 20 73 pm2.61dane ⊢ ( 𝜑 → ( 𝑃 ‘ 𝐴 ) ≤ ( 𝑃 ‘ 𝐵 ) )