Metamath Proof Explorer

Theorem ovolfioo

Description: Unpack the interval covering property of the outer measure definition. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolfioo 
|- ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. F ) <-> A. z e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )

Proof

Step Hyp Ref Expression
1 ioof 
 |-  (,) : ( RR* X. RR* ) --> ~P RR
2 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
3 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
4 2 3 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
5 fss 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* ) ) -> F : NN --> ( RR* X. RR* ) )
6 4 5 mpan2 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F : NN --> ( RR* X. RR* ) )
7 fco 
 |-  ( ( (,) : ( RR* X. RR* ) --> ~P RR /\ F : NN --> ( RR* X. RR* ) ) -> ( (,) o. F ) : NN --> ~P RR )
8 1 6 7 sylancr 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( (,) o. F ) : NN --> ~P RR )
9 ffn 
 |-  ( ( (,) o. F ) : NN --> ~P RR -> ( (,) o. F ) Fn NN )
10 fniunfv 
 |-  ( ( (,) o. F ) Fn NN -> U_ n e. NN ( ( (,) o. F ) ` n ) = U. ran ( (,) o. F ) )
11 8 9 10 3syl 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U_ n e. NN ( ( (,) o. F ) ` n ) = U. ran ( (,) o. F ) )
12 11 sseq2d 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( A C_ U_ n e. NN ( ( (,) o. F ) ` n ) <-> A C_ U. ran ( (,) o. F ) ) )
13 12 adantl 
 |-  ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U_ n e. NN ( ( (,) o. F ) ` n ) <-> A C_ U. ran ( (,) o. F ) ) )
14 dfss3 
 |-  ( A C_ U_ n e. NN ( ( (,) o. F ) ` n ) <-> A. z e. A z e. U_ n e. NN ( ( (,) o. F ) ` n ) )
15 ssel2 
 |-  ( ( A C_ RR /\ z e. A ) -> z e. RR )
16 eliun 
 |-  ( z e. U_ n e. NN ( ( (,) o. F ) ` n ) <-> E. n e. NN z e. ( ( (,) o. F ) ` n ) )
17 rexr 
 |-  ( z e. RR -> z e. RR* )
18 17 ad2antrr 
 |-  ( ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) /\ n e. NN ) -> z e. RR* )
19 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( (,) o. F ) ` n ) = ( (,) ` ( F ` n ) ) )
20 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
21 20 elin2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( RR X. RR ) )
22 1st2nd2 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
23 21 22 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
24 23 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( (,) ` ( F ` n ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
25 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) = ( (,) ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
26 24 25 eqtr4di 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( (,) ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
27 19 26 eqtrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( (,) o. F ) ` n ) = ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) )
28 27 eleq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( z e. ( ( (,) o. F ) ` n ) <-> z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) ) )
29 ovolfcl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) )
30 rexr 
 |-  ( ( 1st ` ( F ` n ) ) e. RR -> ( 1st ` ( F ` n ) ) e. RR* )
31 rexr 
 |-  ( ( 2nd ` ( F ` n ) ) e. RR -> ( 2nd ` ( F ` n ) ) e. RR* )
32 elioo1 
 |-  ( ( ( 1st ` ( F ` n ) ) e. RR* /\ ( 2nd ` ( F ` n ) ) e. RR* ) -> ( z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
33 30 31 32 syl2an 
 |-  ( ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR ) -> ( z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
34 3anass 
 |-  ( ( z e. RR* /\ ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
35 33 34 bitrdi 
 |-  ( ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR ) -> ( z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) ) )
36 35 3adant3 
 |-  ( ( ( 1st ` ( F ` n ) ) e. RR /\ ( 2nd ` ( F ` n ) ) e. RR /\ ( 1st ` ( F ` n ) ) <_ ( 2nd ` ( F ` n ) ) ) -> ( z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) ) )
37 29 36 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( z e. ( ( 1st ` ( F ` n ) ) (,) ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) ) )
38 28 37 bitrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( z e. ( ( (,) o. F ) ` n ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) ) )
39 38 adantll 
 |-  ( ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) /\ n e. NN ) -> ( z e. ( ( (,) o. F ) ` n ) <-> ( z e. RR* /\ ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) ) )
40 18 39 mpbirand 
 |-  ( ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) /\ n e. NN ) -> ( z e. ( ( (,) o. F ) ` n ) <-> ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
41 40 rexbidva 
 |-  ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( E. n e. NN z e. ( ( (,) o. F ) ` n ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
42 16 41 syl5bb 
 |-  ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( z e. U_ n e. NN ( ( (,) o. F ) ` n ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
43 15 42 sylan 
 |-  ( ( ( A C_ RR /\ z e. A ) /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( z e. U_ n e. NN ( ( (,) o. F ) ` n ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
44 43 an32s 
 |-  ( ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) /\ z e. A ) -> ( z e. U_ n e. NN ( ( (,) o. F ) ` n ) <-> E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
45 44 ralbidva 
 |-  ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A. z e. A z e. U_ n e. NN ( ( (,) o. F ) ` n ) <-> A. z e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
46 14 45 syl5bb 
 |-  ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U_ n e. NN ( ( (,) o. F ) ` n ) <-> A. z e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )
47 13 46 bitr3d 
 |-  ( ( A C_ RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. F ) <-> A. z e. A E. n e. NN ( ( 1st ` ( F ` n ) ) < z /\ z < ( 2nd ` ( F ` n ) ) ) ) )