Metamath Proof Explorer

Theorem ovnsupge0

Description: The set used in the definition of the Lebesgue outer measure is a subset of the nonnegative extended reals. This is a substep for (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnsupge0.1 
|- ( ph -> X e. Fin )
ovnsupge0.2 
|- ( ph -> A C_ ( RR ^m X ) )
ovnsupge0.3 
|- 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 ) ) ) ) ) }
Assertion ovnsupge0 
|- ( ph -> M C_ ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 ovnsupge0.1 
 |-  ( ph -> X e. Fin )
2 ovnsupge0.2 
 |-  ( ph -> A C_ ( RR ^m X ) )
3 ovnsupge0.3 
 |-  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 ) ) ) ) ) }
4 simp3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ 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 ) ) ) ) )
5 nnex 
 |-  NN e. _V
6 5 a1i 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> NN e. _V )
7 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
8 nfv 
 |-  F/ k ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN )
9 1 ad2antrr 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN ) -> X e. Fin )
10 elmapi 
 |-  ( i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) )
11 10 ad2antlr 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN ) -> i : NN --> ( ( RR X. RR ) ^m X ) )
12 simpr 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN ) -> j e. NN )
13 8 9 11 12 ovnprodcl 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. ( 0 [,) +oo ) )
14 7 13 sseldi 
 |-  ( ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) e. ( 0 [,] +oo ) )
15 eqid 
 |-  ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) )
16 14 15 fmptd 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) : NN --> ( 0 [,] +oo ) )
17 6 16 sge0cl 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) e. ( 0 [,] +oo ) )
18 17 3adant3 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) e. ( 0 [,] +oo ) )
19 4 18 eqeltrd 
 |-  ( ( ph /\ i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) -> z e. ( 0 [,] +oo ) )
20 19 3adant3l 
 |-  ( ( ph /\ 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 ) ) ) ) ) ) -> z e. ( 0 [,] +oo ) )
21 20 3exp 
 |-  ( ph -> ( 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 ) ) ) ) ) -> z e. ( 0 [,] +oo ) ) ) )
22 21 adantr 
 |-  ( ( ph /\ z e. RR* ) -> ( 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 ) ) ) ) ) -> z e. ( 0 [,] +oo ) ) ) )
23 22 rexlimdv 
 |-  ( ( ph /\ 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 ) ) ) ) ) -> z e. ( 0 [,] +oo ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. 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 ) ) ) ) ) -> z e. ( 0 [,] +oo ) ) )
25 rabss 
 |-  ( { 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_ ( 0 [,] +oo ) <-> A. 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 ) ) ) ) ) -> z e. ( 0 [,] +oo ) ) )
26 24 25 sylibr 
 |-  ( ph -> { 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_ ( 0 [,] +oo ) )
27 3 26 eqsstrid 
 |-  ( ph -> M C_ ( 0 [,] +oo ) )