Metamath Proof Explorer

Theorem omsmon

Description: A constructed outer measure is monotone. Note in Example 1.5.2 of Bogachev p. 17. (Contributed by Thierry Arnoux, 15-Sep-2019) (Revised by AV, 4-Oct-2020)

Ref Expression
Hypotheses oms.m 
|- M = ( toOMeas ` R )
oms.o 
|- ( ph -> Q e. V )
oms.r 
|- ( ph -> R : Q --> ( 0 [,] +oo ) )
omsmon.a 
|- ( ph -> A C_ B )
omsmon.b 
|- ( ph -> B C_ U. Q )
Assertion omsmon 
|- ( ph -> ( M ` A ) <_ ( M ` B ) )

Proof

Step Hyp Ref Expression
1 oms.m 
 |-  M = ( toOMeas ` R )
2 oms.o 
 |-  ( ph -> Q e. V )
3 oms.r 
 |-  ( ph -> R : Q --> ( 0 [,] +oo ) )
4 omsmon.a 
 |-  ( ph -> A C_ B )
5 omsmon.b 
 |-  ( ph -> B C_ U. Q )
6 4 adantr 
 |-  ( ( ph /\ z e. ~P dom R ) -> A C_ B )
7 sstr2 
 |-  ( A C_ B -> ( B C_ U. z -> A C_ U. z ) )
8 6 7 syl 
 |-  ( ( ph /\ z e. ~P dom R ) -> ( B C_ U. z -> A C_ U. z ) )
9 8 anim1d 
 |-  ( ( ph /\ z e. ~P dom R ) -> ( ( B C_ U. z /\ z ~<_ _om ) -> ( A C_ U. z /\ z ~<_ _om ) ) )
10 9 ss2rabdv 
 |-  ( ph -> { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } C_ { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } )
11 resmpt 
 |-  ( { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } C_ { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } -> ( ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) |` { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } ) = ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
12 10 11 syl 
 |-  ( ph -> ( ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) |` { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } ) = ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
13 resss 
 |-  ( ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) |` { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } ) C_ ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
14 12 13 eqsstrrdi 
 |-  ( ph -> ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
15 rnss 
 |-  ( ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) -> ran ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
16 14 15 syl 
 |-  ( ph -> ran ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) )
17 3 ad2antrr 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> R : Q --> ( 0 [,] +oo ) )
18 ssrab2 
 |-  { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } C_ ~P dom R
19 simplr 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } )
20 18 19 sseldi 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> x e. ~P dom R )
21 elpwi 
 |-  ( x e. ~P dom R -> x C_ dom R )
22 20 21 syl 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> x C_ dom R )
23 3 fdmd 
 |-  ( ph -> dom R = Q )
24 23 ad2antrr 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> dom R = Q )
25 22 24 sseqtrd 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> x C_ Q )
26 simpr 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> y e. x )
27 25 26 sseldd 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> y e. Q )
28 17 27 ffvelrnd 
 |-  ( ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) /\ y e. x ) -> ( R ` y ) e. ( 0 [,] +oo ) )
29 28 ralrimiva 
 |-  ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> A. y e. x ( R ` y ) e. ( 0 [,] +oo ) )
30 vex 
 |-  x e. _V
31 nfcv 
 |-  F/_ y x
32 31 esumcl 
 |-  ( ( x e. _V /\ A. y e. x ( R ` y ) e. ( 0 [,] +oo ) ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
33 30 32 mpan 
 |-  ( A. y e. x ( R ` y ) e. ( 0 [,] +oo ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
34 29 33 syl 
 |-  ( ( ph /\ x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } ) -> sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
35 34 ralrimiva 
 |-  ( ph -> A. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) )
36 eqid 
 |-  ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) = ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) )
37 36 rnmptss 
 |-  ( A. x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } sum* y e. x ( R ` y ) e. ( 0 [,] +oo ) -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
38 35 37 syl 
 |-  ( ph -> ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) C_ ( 0 [,] +oo ) )
39 16 38 xrge0infssd 
 |-  ( ph -> inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) <_ inf ( ran ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
40 4 5 sstrd 
 |-  ( ph -> A C_ U. Q )
41 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ A C_ U. Q ) -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
42 2 3 40 41 syl3anc 
 |-  ( ph -> ( ( toOMeas ` R ) ` A ) = inf ( ran ( x e. { z e. ~P dom R | ( A C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
43 omsfval 
 |-  ( ( Q e. V /\ R : Q --> ( 0 [,] +oo ) /\ B C_ U. Q ) -> ( ( toOMeas ` R ) ` B ) = inf ( ran ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
44 2 3 5 43 syl3anc 
 |-  ( ph -> ( ( toOMeas ` R ) ` B ) = inf ( ran ( x e. { z e. ~P dom R | ( B C_ U. z /\ z ~<_ _om ) } |-> sum* y e. x ( R ` y ) ) , ( 0 [,] +oo ) , < ) )
45 39 42 44 3brtr4d 
 |-  ( ph -> ( ( toOMeas ` R ) ` A ) <_ ( ( toOMeas ` R ) ` B ) )
46 1 fveq1i 
 |-  ( M ` A ) = ( ( toOMeas ` R ) ` A )
47 1 fveq1i 
 |-  ( M ` B ) = ( ( toOMeas ` R ) ` B )
48 45 46 47 3brtr4g 
 |-  ( ph -> ( M ` A ) <_ ( M ` B ) )