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 id 
 |-  ( 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 11 ad2antll 
 |-  ( ( 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 ) ) ) ) )
13 10 12 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 ) ) ) ) ) )
14 13 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 ) ) ) ) ) ) )
15 14 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 ) ) ) ) ) ) )
16 15 ralrimivw 
 |-  ( ph -> A. 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 ) ) ) ) ) ) )
17 ss2rab 
 |-  ( { 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 ) ) ) ) ) } <-> A. 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 ) ) ) ) ) ) )
18 16 17 sylibr 
 |-  ( 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 ) ) ) ) ) } )
19 6 a1i 
 |-  ( ph -> 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 ) ) ) ) ) } )
20 5 a1i 
 |-  ( ph -> 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 ) ) ) ) ) } )
21 19 20 sseq12d 
 |-  ( ph -> ( N C_ M <-> { 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 ) ) ) ) ) } ) )
22 18 21 mpbird 
 |-  ( ph -> N C_ M )
23 ssrab2 
 |-  { 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 ) ) ) ) ) } C_ RR*
24 5 23 eqsstri 
 |-  M C_ RR*
25 24 a1i 
 |-  ( ph -> M C_ RR* )
26 infxrss 
 |-  ( ( N C_ M /\ M C_ RR* ) -> inf ( M , RR* , < ) <_ inf ( N , RR* , < ) )
27 22 25 26 syl2anc 
 |-  ( ph -> inf ( M , RR* , < ) <_ inf ( N , RR* , < ) )
28 3 4 sstrd 
 |-  ( ph -> A C_ ( RR ^m X ) )
29 1 2 28 5 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` A ) = inf ( M , RR* , < ) )
30 1 2 4 6 ovnn0val 
 |-  ( ph -> ( ( voln* ` X ) ` B ) = inf ( N , RR* , < ) )
31 29 30 breq12d 
 |-  ( ph -> ( ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) <-> inf ( M , RR* , < ) <_ inf ( N , RR* , < ) ) )
32 27 31 mpbird 
 |-  ( ph -> ( ( voln* ` X ) ` A ) <_ ( ( voln* ` X ) ` B ) )