Metamath Proof Explorer

Theorem ovnf

Description: The Lebesgue outer measure is a function that maps sets to nonnegative extended reals. This is step (a)(i) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis ovnf.1 
|- ( ph -> X e. Fin )
Assertion ovnf 
|- ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )

Proof

Step Hyp Ref Expression
1 ovnf.1 
 |-  ( ph -> X e. Fin )
2 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
3 2 a1i 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> 0 e. ( 0 [,] +oo ) )
4 0xr 
 |-  0 e. RR*
5 4 a1i 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> 0 e. RR* )
6 pnfxr 
 |-  +oo e. RR*
7 6 a1i 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> +oo e. RR* )
8 1 adantr 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> X e. Fin )
9 elpwi 
 |-  ( y e. ~P ( RR ^m X ) -> y C_ ( RR ^m X ) )
10 9 adantl 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> y C_ ( RR ^m X ) )
11 eqid 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) }
12 8 10 11 ovnsupge0 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) )
13 8 10 11 ovnpnfelsup 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> +oo e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ne0d 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 5 7 12 14 inficc 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) e. ( 0 [,] +oo ) )
16 3 15 ifcld 
 |-  ( ( ph /\ y e. ~P ( RR ^m X ) ) -> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) e. ( 0 [,] +oo ) )
17 eqid 
 |-  ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) ) = ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) )
18 16 17 fmptd 
 |-  ( ph -> ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )
19 1 ovnval 
 |-  ( ph -> ( voln* ` X ) = ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) ) )
20 19 feq1d 
 |-  ( ph -> ( ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) <-> ( y e. ~P ( RR ^m X ) |-> if ( X = (/) , 0 , inf ( { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( y 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 ) ) ) ) ) } , RR* , < ) ) ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) ) )
21 18 20 mpbird 
 |-  ( ph -> ( voln* ` X ) : ~P ( RR ^m X ) --> ( 0 [,] +oo ) )