Metamath Proof Explorer


Theorem dya2iocnei

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 J=topGenran.
dya2ioc.1 I=x,nx2nx+12n
dya2ioc.2 R=uranI,vranIu×v
Assertion dya2iocnei AJ×tJXAbranRXbbA

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 J=topGenran.
2 dya2ioc.1 I=x,nx2nx+12n
3 dya2ioc.2 R=uranI,vranIu×v
4 elunii XAAJ×tJXJ×tJ
5 4 ancoms AJ×tJXAXJ×tJ
6 1 tpr2uni J×tJ=2
7 5 6 eleqtrdi AJ×tJXAX2
8 eqid u,vu+iv=u,vu+iv
9 eqid raneran.,fran.e×f=raneran.,fran.e×f
10 1 8 9 tpr2rico AJ×tJXArraneran.,fran.e×fXrrA
11 anass rraneran.,fran.e×fXrrArraneran.,fran.e×fXrrA
12 1 2 3 9 dya2iocnrect X2rraneran.,fran.e×fXrbranRXbbr
13 12 3expb X2rraneran.,fran.e×fXrbranRXbbr
14 13 anim1i X2rraneran.,fran.e×fXrrAbranRXbbrrA
15 14 anasss X2rraneran.,fran.e×fXrrAbranRXbbrrA
16 11 15 sylan2br X2rraneran.,fran.e×fXrrAbranRXbbrrA
17 r19.41v branRXbbrrAbranRXbbrrA
18 simpll XbbrrAXb
19 simplr XbbrrAbr
20 simpr XbbrrArA
21 19 20 sstrd XbbrrAbA
22 18 21 jca XbbrrAXbbA
23 22 reximi branRXbbrrAbranRXbbA
24 17 23 sylbir branRXbbrrAbranRXbbA
25 16 24 syl X2rraneran.,fran.e×fXrrAbranRXbbA
26 25 rexlimdvaa X2rraneran.,fran.e×fXrrAbranRXbbA
27 7 10 26 sylc AJ×tJXAbranRXbbA