Metamath Proof Explorer

Theorem ovolficcss

Description: Any (closed) interval covering is a subset of the reals. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Assertion ovolficcss 
|- ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )

Proof

Step Hyp Ref Expression
1 rnco2 
 |-  ran ( [,] o. F ) = ( [,] " ran F )
2 ffvelrn 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) e. ( <_ i^i ( RR X. RR ) ) )
3 2 elin2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) e. ( RR X. RR ) )
4 1st2nd2 
 |-  ( ( F ` y ) e. ( RR X. RR ) -> ( F ` y ) = <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. )
5 3 4 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( F ` y ) = <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. )
6 5 fveq2d 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) = ( [,] ` <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. ) )
7 df-ov 
 |-  ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) = ( [,] ` <. ( 1st ` ( F ` y ) ) , ( 2nd ` ( F ` y ) ) >. )
8 6 7 eqtr4di 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) = ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) )
9 xp1st 
 |-  ( ( F ` y ) e. ( RR X. RR ) -> ( 1st ` ( F ` y ) ) e. RR )
10 3 9 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( 1st ` ( F ` y ) ) e. RR )
11 xp2nd 
 |-  ( ( F ` y ) e. ( RR X. RR ) -> ( 2nd ` ( F ` y ) ) e. RR )
12 3 11 syl 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( 2nd ` ( F ` y ) ) e. RR )
13 iccssre 
 |-  ( ( ( 1st ` ( F ` y ) ) e. RR /\ ( 2nd ` ( F ` y ) ) e. RR ) -> ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) C_ RR )
14 10 12 13 syl2anc 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( ( 1st ` ( F ` y ) ) [,] ( 2nd ` ( F ` y ) ) ) C_ RR )
15 8 14 eqsstrd 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) C_ RR )
16 reex 
 |-  RR e. _V
17 16 elpw2 
 |-  ( ( [,] ` ( F ` y ) ) e. ~P RR <-> ( [,] ` ( F ` y ) ) C_ RR )
18 15 17 sylibr 
 |-  ( ( F : NN --> ( <_ i^i ( RR X. RR ) ) /\ y e. NN ) -> ( [,] ` ( F ` y ) ) e. ~P RR )
19 18 ralrimiva 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR )
20 ffn 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> F Fn NN )
21 fveq2 
 |-  ( x = ( F ` y ) -> ( [,] ` x ) = ( [,] ` ( F ` y ) ) )
22 21 eleq1d 
 |-  ( x = ( F ` y ) -> ( ( [,] ` x ) e. ~P RR <-> ( [,] ` ( F ` y ) ) e. ~P RR ) )
23 22 ralrn 
 |-  ( F Fn NN -> ( A. x e. ran F ( [,] ` x ) e. ~P RR <-> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR ) )
24 20 23 syl 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( A. x e. ran F ( [,] ` x ) e. ~P RR <-> A. y e. NN ( [,] ` ( F ` y ) ) e. ~P RR ) )
25 19 24 mpbird 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> A. x e. ran F ( [,] ` x ) e. ~P RR )
26 iccf 
 |-  [,] : ( RR* X. RR* ) --> ~P RR*
27 ffun 
 |-  ( [,] : ( RR* X. RR* ) --> ~P RR* -> Fun [,] )
28 26 27 ax-mp 
 |-  Fun [,]
29 frn 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ ( <_ i^i ( RR X. RR ) ) )
30 inss2 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR X. RR )
31 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
32 30 31 sstri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ ( RR* X. RR* )
33 26 fdmi 
 |-  dom [,] = ( RR* X. RR* )
34 32 33 sseqtrri 
 |-  ( <_ i^i ( RR X. RR ) ) C_ dom [,]
35 29 34 sstrdi 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran F C_ dom [,] )
36 funimass4 
 |-  ( ( Fun [,] /\ ran F C_ dom [,] ) -> ( ( [,] " ran F ) C_ ~P RR <-> A. x e. ran F ( [,] ` x ) e. ~P RR ) )
37 28 35 36 sylancr 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( ( [,] " ran F ) C_ ~P RR <-> A. x e. ran F ( [,] ` x ) e. ~P RR ) )
38 25 37 mpbird 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ( [,] " ran F ) C_ ~P RR )
39 1 38 eqsstrid 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> ran ( [,] o. F ) C_ ~P RR )
40 sspwuni 
 |-  ( ran ( [,] o. F ) C_ ~P RR <-> U. ran ( [,] o. F ) C_ RR )
41 39 40 sylib 
 |-  ( F : NN --> ( <_ i^i ( RR X. RR ) ) -> U. ran ( [,] o. F ) C_ RR )