Description: For any point of an open set of the usual topology on ( RR X. RR ) there is a closed-below open-above dyadic rational square which contains that point and is entirely in the open set. (Contributed by Thierry Arnoux, 21-Sep-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | sxbrsiga.0 | |
|
dya2ioc.1 | |
||
dya2ioc.2 | |
||
Assertion | dya2iocnei | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sxbrsiga.0 | |
|
2 | dya2ioc.1 | |
|
3 | dya2ioc.2 | |
|
4 | elunii | |
|
5 | 4 | ancoms | |
6 | 1 | tpr2uni | |
7 | 5 6 | eleqtrdi | |
8 | eqid | |
|
9 | eqid | |
|
10 | 1 8 9 | tpr2rico | |
11 | anass | |
|
12 | 1 2 3 9 | dya2iocnrect | |
13 | 12 | 3expb | |
14 | 13 | anim1i | |
15 | 14 | anasss | |
16 | 11 15 | sylan2br | |
17 | r19.41v | |
|
18 | simpll | |
|
19 | simplr | |
|
20 | simpr | |
|
21 | 19 20 | sstrd | |
22 | 18 21 | jca | |
23 | 22 | reximi | |
24 | 17 23 | sylbir | |
25 | 16 24 | syl | |
26 | 25 | rexlimdvaa | |
27 | 7 10 26 | sylc | |