Metamath Proof Explorer

Theorem icoreunrn

Description: The union of all closed-below, open-above intervals of reals is the set of reals. (Contributed by ML, 27-Jul-2020)

Ref Expression
Hypothesis icoreunrn.1 
|- I = ( [,) " ( RR X. RR ) )
Assertion icoreunrn 
|- RR = U. I

Proof

Step Hyp Ref Expression
1 icoreunrn.1 
 |-  I = ( [,) " ( RR X. RR ) )
2 rexr 
 |-  ( x e. RR -> x e. RR* )
3 peano2re 
 |-  ( x e. RR -> ( x + 1 ) e. RR )
4 rexr 
 |-  ( ( x + 1 ) e. RR -> ( x + 1 ) e. RR* )
5 3 4 syl 
 |-  ( x e. RR -> ( x + 1 ) e. RR* )
6 ltp1 
 |-  ( x e. RR -> x < ( x + 1 ) )
7 lbico1 
 |-  ( ( x e. RR* /\ ( x + 1 ) e. RR* /\ x < ( x + 1 ) ) -> x e. ( x [,) ( x + 1 ) ) )
8 2 5 6 7 syl3anc 
 |-  ( x e. RR -> x e. ( x [,) ( x + 1 ) ) )
9 df-ov 
 |-  ( x [,) ( x + 1 ) ) = ( [,) ` <. x , ( x + 1 ) >. )
10 8 9 eleqtrdi 
 |-  ( x e. RR -> x e. ( [,) ` <. x , ( x + 1 ) >. ) )
11 opelxpi 
 |-  ( ( x e. RR /\ ( x + 1 ) e. RR ) -> <. x , ( x + 1 ) >. e. ( RR X. RR ) )
12 3 11 mpdan 
 |-  ( x e. RR -> <. x , ( x + 1 ) >. e. ( RR X. RR ) )
13 fvres 
 |-  ( <. x , ( x + 1 ) >. e. ( RR X. RR ) -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) = ( [,) ` <. x , ( x + 1 ) >. ) )
14 12 13 syl 
 |-  ( x e. RR -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) = ( [,) ` <. x , ( x + 1 ) >. ) )
15 10 14 eleqtrrd 
 |-  ( x e. RR -> x e. ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) )
16 icoreresf 
 |-  ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR
17 16 fdmi 
 |-  dom ( [,) |` ( RR X. RR ) ) = ( RR X. RR )
18 11 17 eleqtrrdi 
 |-  ( ( x e. RR /\ ( x + 1 ) e. RR ) -> <. x , ( x + 1 ) >. e. dom ( [,) |` ( RR X. RR ) ) )
19 3 18 mpdan 
 |-  ( x e. RR -> <. x , ( x + 1 ) >. e. dom ( [,) |` ( RR X. RR ) ) )
20 ffun 
 |-  ( ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR -> Fun ( [,) |` ( RR X. RR ) ) )
21 16 20 ax-mp 
 |-  Fun ( [,) |` ( RR X. RR ) )
22 fvelrn 
 |-  ( ( Fun ( [,) |` ( RR X. RR ) ) /\ <. x , ( x + 1 ) >. e. dom ( [,) |` ( RR X. RR ) ) ) -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) e. ran ( [,) |` ( RR X. RR ) ) )
23 21 22 mpan 
 |-  ( <. x , ( x + 1 ) >. e. dom ( [,) |` ( RR X. RR ) ) -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) e. ran ( [,) |` ( RR X. RR ) ) )
24 df-ima 
 |-  ( [,) " ( RR X. RR ) ) = ran ( [,) |` ( RR X. RR ) )
25 1 24 eqtri 
 |-  I = ran ( [,) |` ( RR X. RR ) )
26 23 25 eleqtrrdi 
 |-  ( <. x , ( x + 1 ) >. e. dom ( [,) |` ( RR X. RR ) ) -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) e. I )
27 19 26 syl 
 |-  ( x e. RR -> ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) e. I )
28 elunii 
 |-  ( ( x e. ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) /\ ( ( [,) |` ( RR X. RR ) ) ` <. x , ( x + 1 ) >. ) e. I ) -> x e. U. I )
29 15 27 28 syl2anc 
 |-  ( x e. RR -> x e. U. I )
30 29 ssriv 
 |-  RR C_ U. I
31 frn 
 |-  ( ( [,) |` ( RR X. RR ) ) : ( RR X. RR ) --> ~P RR -> ran ( [,) |` ( RR X. RR ) ) C_ ~P RR )
32 16 31 ax-mp 
 |-  ran ( [,) |` ( RR X. RR ) ) C_ ~P RR
33 25 32 eqsstri 
 |-  I C_ ~P RR
34 uniss 
 |-  ( I C_ ~P RR -> U. I C_ U. ~P RR )
35 unipw 
 |-  U. ~P RR = RR
36 34 35 sseqtrdi 
 |-  ( I C_ ~P RR -> U. I C_ RR )
37 33 36 ax-mp 
 |-  U. I C_ RR
38 30 37 eqssi 
 |-  RR = U. I