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 
|- ( ph -> P : R --> ( 0 [,] +oo ) )
caraext.2 
|- ( ph -> ( P ` (/) ) = 0 )
caraext.3 
|- ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) )
pmeasmono.1 
|- ( ph -> A e. R )
pmeasmono.2 
|- ( ph -> B e. R )
pmeasmono.3 
|- ( ph -> ( B \ A ) e. R )
pmeasmono.4 
|- ( ph -> A C_ B )
Assertion pmeasmono 
|- ( ph -> ( P ` A ) <_ ( P ` B ) )

Proof

Step Hyp Ref Expression
1 caraext.1 
 |-  ( ph -> P : R --> ( 0 [,] +oo ) )
2 caraext.2 
 |-  ( ph -> ( P ` (/) ) = 0 )
3 caraext.3 
 |-  ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) )
4 pmeasmono.1 
 |-  ( ph -> A e. R )
5 pmeasmono.2 
 |-  ( ph -> B e. R )
6 pmeasmono.3 
 |-  ( ph -> ( B \ A ) e. R )
7 pmeasmono.4 
 |-  ( ph -> A C_ B )
8 eqimss 
 |-  ( A = ( B \ A ) -> A C_ ( B \ A ) )
9 ssdifeq0 
 |-  ( A C_ ( B \ A ) <-> A = (/) )
10 8 9 sylib 
 |-  ( A = ( B \ A ) -> A = (/) )
11 10 fveq2d 
 |-  ( A = ( B \ A ) -> ( P ` A ) = ( P ` (/) ) )
12 11 adantl 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( P ` A ) = ( P ` (/) ) )
13 2 adantr 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( P ` (/) ) = 0 )
14 12 13 eqtrd 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( P ` A ) = 0 )
15 1 5 ffvelrnd 
 |-  ( ph -> ( P ` B ) e. ( 0 [,] +oo ) )
16 elxrge0 
 |-  ( ( P ` B ) e. ( 0 [,] +oo ) <-> ( ( P ` B ) e. RR* /\ 0 <_ ( P ` B ) ) )
17 16 simprbi 
 |-  ( ( P ` B ) e. ( 0 [,] +oo ) -> 0 <_ ( P ` B ) )
18 15 17 syl 
 |-  ( ph -> 0 <_ ( P ` B ) )
19 18 adantr 
 |-  ( ( ph /\ A = ( B \ A ) ) -> 0 <_ ( P ` B ) )
20 14 19 eqbrtrd 
 |-  ( ( ph /\ A = ( B \ A ) ) -> ( P ` A ) <_ ( P ` B ) )
21 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
22 1 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> P : R --> ( 0 [,] +oo ) )
23 4 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> A e. R )
24 22 23 ffvelrnd 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` A ) e. ( 0 [,] +oo ) )
25 21 24 sseldi 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` A ) e. RR* )
26 6 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( B \ A ) e. R )
27 22 26 ffvelrnd 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` ( B \ A ) ) e. ( 0 [,] +oo ) )
28 xrge0addge 
 |-  ( ( ( P ` A ) e. RR* /\ ( P ` ( B \ A ) ) e. ( 0 [,] +oo ) ) -> ( P ` A ) <_ ( ( P ` A ) +e ( P ` ( B \ A ) ) ) )
29 25 27 28 syl2anc 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` A ) <_ ( ( P ` A ) +e ( P ` ( B \ A ) ) ) )
30 prct 
 |-  ( ( A e. R /\ ( B \ A ) e. R ) -> { A , ( B \ A ) } ~<_ _om )
31 4 6 30 syl2anc 
 |-  ( ph -> { A , ( B \ A ) } ~<_ _om )
32 31 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> { A , ( B \ A ) } ~<_ _om )
33 prssi 
 |-  ( ( A e. R /\ ( B \ A ) e. R ) -> { A , ( B \ A ) } C_ R )
34 4 6 33 syl2anc 
 |-  ( ph -> { A , ( B \ A ) } C_ R )
35 34 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> { A , ( B \ A ) } C_ R )
36 disjdif 
 |-  ( A i^i ( B \ A ) ) = (/)
37 simpr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> A =/= ( B \ A ) )
38 id 
 |-  ( y = A -> y = A )
39 id 
 |-  ( y = ( B \ A ) -> y = ( B \ A ) )
40 38 39 disjprg 
 |-  ( ( A e. R /\ ( B \ A ) e. R /\ A =/= ( B \ A ) ) -> ( Disj_ y e. { A , ( B \ A ) } y <-> ( A i^i ( B \ A ) ) = (/) ) )
41 23 26 37 40 syl3anc 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( Disj_ y e. { A , ( B \ A ) } y <-> ( A i^i ( B \ A ) ) = (/) ) )
42 36 41 mpbiri 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> Disj_ y e. { A , ( B \ A ) } y )
43 32 35 42 3jca 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) )
44 prex 
 |-  { A , ( B \ A ) } e. _V
45 biidd 
 |-  ( x = { A , ( B \ A ) } -> ( ph <-> ph ) )
46 breq1 
 |-  ( x = { A , ( B \ A ) } -> ( x ~<_ _om <-> { A , ( B \ A ) } ~<_ _om ) )
47 sseq1 
 |-  ( x = { A , ( B \ A ) } -> ( x C_ R <-> { A , ( B \ A ) } C_ R ) )
48 disjeq1 
 |-  ( x = { A , ( B \ A ) } -> ( Disj_ y e. x y <-> Disj_ y e. { A , ( B \ A ) } y ) )
49 46 47 48 3anbi123d 
 |-  ( x = { A , ( B \ A ) } -> ( ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) <-> ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) )
50 45 49 anbi12d 
 |-  ( x = { A , ( B \ A ) } -> ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) <-> ( ph /\ ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) ) )
51 unieq 
 |-  ( x = { A , ( B \ A ) } -> U. x = U. { A , ( B \ A ) } )
52 51 fveq2d 
 |-  ( x = { A , ( B \ A ) } -> ( P ` U. x ) = ( P ` U. { A , ( B \ A ) } ) )
53 esumeq1 
 |-  ( x = { A , ( B \ A ) } -> sum* y e. x ( P ` y ) = sum* y e. { A , ( B \ A ) } ( P ` y ) )
54 52 53 eqeq12d 
 |-  ( x = { A , ( B \ A ) } -> ( ( P ` U. x ) = sum* y e. x ( P ` y ) <-> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) ) )
55 50 54 imbi12d 
 |-  ( x = { A , ( B \ A ) } -> ( ( ( ph /\ ( x ~<_ _om /\ x C_ R /\ Disj_ y e. x y ) ) -> ( P ` U. x ) = sum* y e. x ( P ` y ) ) <-> ( ( ph /\ ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) -> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) ) ) )
56 55 3 vtoclg 
 |-  ( { A , ( B \ A ) } e. _V -> ( ( ph /\ ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) -> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) ) )
57 44 56 ax-mp 
 |-  ( ( ph /\ ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) -> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) )
58 57 adantlr 
 |-  ( ( ( ph /\ A =/= ( B \ A ) ) /\ ( { A , ( B \ A ) } ~<_ _om /\ { A , ( B \ A ) } C_ R /\ Disj_ y e. { A , ( B \ A ) } y ) ) -> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) )
59 43 58 mpdan 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` U. { A , ( B \ A ) } ) = sum* y e. { A , ( B \ A ) } ( P ` y ) )
60 uniprg 
 |-  ( ( A e. R /\ ( B \ A ) e. R ) -> U. { A , ( B \ A ) } = ( A u. ( B \ A ) ) )
61 4 6 60 syl2anc 
 |-  ( ph -> U. { A , ( B \ A ) } = ( A u. ( B \ A ) ) )
62 undif 
 |-  ( A C_ B <-> ( A u. ( B \ A ) ) = B )
63 7 62 sylib 
 |-  ( ph -> ( A u. ( B \ A ) ) = B )
64 61 63 eqtrd 
 |-  ( ph -> U. { A , ( B \ A ) } = B )
65 64 adantr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> U. { A , ( B \ A ) } = B )
66 65 fveq2d 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` U. { A , ( B \ A ) } ) = ( P ` B ) )
67 simpr 
 |-  ( ( ( ph /\ A =/= ( B \ A ) ) /\ y = A ) -> y = A )
68 67 fveq2d 
 |-  ( ( ( ph /\ A =/= ( B \ A ) ) /\ y = A ) -> ( P ` y ) = ( P ` A ) )
69 simpr 
 |-  ( ( ( ph /\ A =/= ( B \ A ) ) /\ y = ( B \ A ) ) -> y = ( B \ A ) )
70 69 fveq2d 
 |-  ( ( ( ph /\ A =/= ( B \ A ) ) /\ y = ( B \ A ) ) -> ( P ` y ) = ( P ` ( B \ A ) ) )
71 68 70 23 26 24 27 37 esumpr 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> sum* y e. { A , ( B \ A ) } ( P ` y ) = ( ( P ` A ) +e ( P ` ( B \ A ) ) ) )
72 59 66 71 3eqtr3d 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` B ) = ( ( P ` A ) +e ( P ` ( B \ A ) ) ) )
73 29 72 breqtrrd 
 |-  ( ( ph /\ A =/= ( B \ A ) ) -> ( P ` A ) <_ ( P ` B ) )
74 20 73 pm2.61dane 
 |-  ( ph -> ( P ` A ) <_ ( P ` B ) )