Metamath Proof Explorer

Theorem ovnsslelem

Description: The (multidimensional, nonzero-dimensional) Lebesgue outer measure of a subset is less than the L.o.m. of the whole set. This is step (iii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsslelem.1 
|- ( ph -> X e. Fin )
ovnsslelem.2 
|- ( ph -> X =/= (/) )
ovnsslelem.3 
|- ( ph -> A C_ B )
ovnsslelem.4 
|- ( ph -> B C_ ( RR ^m X ) )
ovnsslelem.5 
|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
ovnsslelem.6 
|- N = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
Assertion ovnsslelem 
|- ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )

Proof

Step Hyp Ref Expression
1 ovnsslelem.1 
 |-  ( ph -> X e. Fin )
2 ovnsslelem.2 
 |-  ( ph -> X =/= (/) )
3 ovnsslelem.3 
 |-  ( ph -> A C_ B )
4 ovnsslelem.4 
 |-  ( ph -> B C_ ( RR ^m X ) )
5 ovnsslelem.5 
 |-  M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
6 ovnsslelem.6 
 |-  N = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
7 3 adantr 
 |-  ( ( ph /\ B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> A C_ B )
8 simpr 
 |-  ( ( ph /\ B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
9 7 8 sstrd 
 |-  ( ( ph /\ B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) ) -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
10 9 adantrr 
 |-  ( ( ph /\ ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) )
11 simprr 
 |-  ( ( ph /\ ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
12 10 11 jca 
 |-  ( ( ph /\ ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
13 12 ex 
 |-  ( ph -> ( ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
14 13 reximdv 
 |-  ( ph -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
15 14 adantr 
 |-  ( ( ph /\ z e. RR* ) -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
16 15 ss2rabdv 
 |-  ( ph -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( B C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
17 16 6 5 3sstr4g 
 |-  ( ph -> N C_ M )
18 5 ssrab3 
 |-  M C_ RR*
19 infxrss 
 |-  ( ( N C_ M /\ M C_ RR* ) -> inf ( M , RR* , < ) <_ inf ( N , RR* , < ) )
20 17 18 19 sylancl 
 |-  ( ph -> inf ( M , RR* , < ) <_ inf ( N , RR* , < ) )
21 3 4 sstrd 
 |-  ( ph -> A C_ ( RR ^m X ) )
22 1 2 21 5 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` A ) = inf ( M , RR* , < ) )
23 1 2 4 6 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` B ) = inf ( N , RR* , < ) )
24 20 22 23 3brtr4d 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )