Metamath Proof Explorer

Theorem ovolficc

Description: Unpack the interval covering property using closed intervals. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolficc 
|- ( ( 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 iccf 
 |-  [,] : ( 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 simpll 
 |-  ( ( ( z e. RR /\ F : NN --> ( <_ i^i ( RR X. RR ) ) ) /\ n e. NN ) -> z e. RR )
18 fvco3 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( [,] o. F ) ` n ) = ( [,] ` ( F ` n ) ) )
19 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( <_ i^i ( RR X. RR ) ) )
20 19 elin2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) e. ( RR X. RR ) )
21 1st2nd2 
 |-  ( ( F ` n ) e. ( RR X. RR ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
22 20 21 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( F ` n ) = <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
23 22 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( [,] ` ( F ` n ) ) = ( [,] ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. ) )
24 df-ov 
 |-  ( ( 1st ` ( F ` n ) ) [,] ( 2nd ` ( F ` n ) ) ) = ( [,] ` <. ( 1st ` ( F ` n ) ) , ( 2nd ` ( F ` n ) ) >. )
25 23 24 eqtr4di 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( [,] ` ( F ` n ) ) = ( ( 1st ` ( F ` n ) ) [,] ( 2nd ` ( F ` n ) ) ) )
26 18 25 eqtrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( ( [,] o. F ) ` n ) = ( ( 1st ` ( F ` n ) ) [,] ( 2nd ` ( F ` n ) ) ) )
27 26 eleq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ n e. NN ) -> ( z e. ( ( [,] o. F ) ` n ) <-> z e. ( ( 1st ` ( F ` n ) ) [,] ( 2nd ` ( F ` n ) ) ) ) )
28 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 ) ) ) )
29 elicc2 
 |-  ( ( ( 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 ) ) ) ) )
30 3anass 
 |-  ( ( z e. RR /\ ( 1st ` ( F ` n ) ) <_ z /\ z <_ ( 2nd ` ( F ` n ) ) ) <-> ( z e. RR /\ ( ( 1st ` ( F ` n ) ) <_ z /\ z <_ ( 2nd ` ( F ` n ) ) ) ) )
31 29 30 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 ) ) ) ) ) )
32 31 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 ) ) ) ) ) )
33 28 32 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 ) ) ) ) ) )
34 27 33 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 ) ) ) ) ) )
35 34 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 ) ) ) ) ) )
36 17 35 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 ) ) ) ) )
37 36 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 ) ) ) ) )
38 16 37 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 ) ) ) ) )
39 15 38 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 ) ) ) ) )
40 39 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 ) ) ) ) )
41 40 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 ) ) ) ) )
42 14 41 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 ) ) ) ) )
43 13 42 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 ) ) ) ) )