Metamath Proof Explorer

Theorem ovolsslem

Description: Lemma for ovolss . (Contributed by Mario Carneiro, 16-Mar-2014) (Proof shortened by AV, 17-Sep-2020)

Ref Expression
Hypotheses ovolss.1 
|- M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
ovolss.2 
|- N = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
Assertion ovolsslem 
|- ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )

Proof

Step Hyp Ref Expression
1 ovolss.1 
 |-  M = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
2 ovolss.2 
 |-  N = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
3 sstr2 
 |-  ( A C_ B -> ( B C_ U. ran ( (,) o. f ) -> A C_ U. ran ( (,) o. f ) ) )
4 3 ad2antrr 
 |-  ( ( ( A C_ B /\ B C_ RR ) /\ y e. RR* ) -> ( B C_ U. ran ( (,) o. f ) -> A C_ U. ran ( (,) o. f ) ) )
5 4 anim1d 
 |-  ( ( ( A C_ B /\ B C_ RR ) /\ y e. RR* ) -> ( ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
6 5 reximdv 
 |-  ( ( ( A C_ B /\ B C_ RR ) /\ y e. RR* ) -> ( E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) -> E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) ) )
7 6 ss2rabdv 
 |-  ( ( A C_ B /\ B C_ RR ) -> { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } C_ { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } )
8 7 2 1 3sstr4g 
 |-  ( ( A C_ B /\ B C_ RR ) -> N C_ M )
9 sstr 
 |-  ( ( A C_ B /\ B C_ RR ) -> A C_ RR )
10 1 ovolval 
 |-  ( A C_ RR -> ( vol* ` A ) = inf ( M , RR* , < ) )
11 10 adantr 
 |-  ( ( A C_ RR /\ x e. M ) -> ( vol* ` A ) = inf ( M , RR* , < ) )
12 1 ssrab3 
 |-  M C_ RR*
13 infxrlb 
 |-  ( ( M C_ RR* /\ x e. M ) -> inf ( M , RR* , < ) <_ x )
14 12 13 mpan 
 |-  ( x e. M -> inf ( M , RR* , < ) <_ x )
15 14 adantl 
 |-  ( ( A C_ RR /\ x e. M ) -> inf ( M , RR* , < ) <_ x )
16 11 15 eqbrtrd 
 |-  ( ( A C_ RR /\ x e. M ) -> ( vol* ` A ) <_ x )
17 16 ralrimiva 
 |-  ( A C_ RR -> A. x e. M ( vol* ` A ) <_ x )
18 9 17 syl 
 |-  ( ( A C_ B /\ B C_ RR ) -> A. x e. M ( vol* ` A ) <_ x )
19 ssralv 
 |-  ( N C_ M -> ( A. x e. M ( vol* ` A ) <_ x -> A. x e. N ( vol* ` A ) <_ x ) )
20 8 18 19 sylc 
 |-  ( ( A C_ B /\ B C_ RR ) -> A. x e. N ( vol* ` A ) <_ x )
21 2 ssrab3 
 |-  N C_ RR*
22 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
23 9 22 syl 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) e. RR* )
24 infxrgelb 
 |-  ( ( N C_ RR* /\ ( vol* ` A ) e. RR* ) -> ( ( vol* ` A ) <_ inf ( N , RR* , < ) <-> A. x e. N ( vol* ` A ) <_ x ) )
25 21 23 24 sylancr 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( ( vol* ` A ) <_ inf ( N , RR* , < ) <-> A. x e. N ( vol* ` A ) <_ x ) )
26 20 25 mpbird 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ inf ( N , RR* , < ) )
27 2 ovolval 
 |-  ( B C_ RR -> ( vol* ` B ) = inf ( N , RR* , < ) )
28 27 adantl 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` B ) = inf ( N , RR* , < ) )
29 26 28 breqtrrd 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )