# 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}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
dya2ioc.1 ${⊢}{I}=\left({x}\in ℤ,{n}\in ℤ⟼\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)$
dya2ioc.2 ${⊢}{R}=\left({u}\in \mathrm{ran}{I},{v}\in \mathrm{ran}{I}⟼{u}×{v}\right)$
Assertion dya2iocnei ${⊢}\left({A}\in \left({J}{×}_{t}{J}\right)\wedge {X}\in {A}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)$

### Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
2 dya2ioc.1 ${⊢}{I}=\left({x}\in ℤ,{n}\in ℤ⟼\left[\frac{{x}}{{2}^{{n}}},\frac{{x}+1}{{2}^{{n}}}\right)\right)$
3 dya2ioc.2 ${⊢}{R}=\left({u}\in \mathrm{ran}{I},{v}\in \mathrm{ran}{I}⟼{u}×{v}\right)$
4 elunii ${⊢}\left({X}\in {A}\wedge {A}\in \left({J}{×}_{t}{J}\right)\right)\to {X}\in \bigcup \left({J}{×}_{t}{J}\right)$
5 4 ancoms ${⊢}\left({A}\in \left({J}{×}_{t}{J}\right)\wedge {X}\in {A}\right)\to {X}\in \bigcup \left({J}{×}_{t}{J}\right)$
6 1 tpr2uni ${⊢}\bigcup \left({J}{×}_{t}{J}\right)={ℝ}^{2}$
7 5 6 eleqtrdi ${⊢}\left({A}\in \left({J}{×}_{t}{J}\right)\wedge {X}\in {A}\right)\to {X}\in {ℝ}^{2}$
8 eqid ${⊢}\left({u}\in ℝ,{v}\in ℝ⟼{u}+\mathrm{i}{v}\right)=\left({u}\in ℝ,{v}\in ℝ⟼{u}+\mathrm{i}{v}\right)$
9 eqid ${⊢}\mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)=\mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)$
10 1 8 9 tpr2rico ${⊢}\left({A}\in \left({J}{×}_{t}{J}\right)\wedge {X}\in {A}\right)\to \exists {r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in {r}\wedge {r}\subseteq {A}\right)$
11 anass ${⊢}\left(\left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge {X}\in {r}\right)\wedge {r}\subseteq {A}\right)↔\left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge \left({X}\in {r}\wedge {r}\subseteq {A}\right)\right)$
12 1 2 3 9 dya2iocnrect ${⊢}\left({X}\in {ℝ}^{2}\wedge {r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge {X}\in {r}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)$
13 12 3expb ${⊢}\left({X}\in {ℝ}^{2}\wedge \left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge {X}\in {r}\right)\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)$
14 13 anim1i ${⊢}\left(\left({X}\in {ℝ}^{2}\wedge \left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge {X}\in {r}\right)\right)\wedge {r}\subseteq {A}\right)\to \left(\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)$
15 14 anasss ${⊢}\left({X}\in {ℝ}^{2}\wedge \left(\left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge {X}\in {r}\right)\wedge {r}\subseteq {A}\right)\right)\to \left(\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)$
16 11 15 sylan2br ${⊢}\left({X}\in {ℝ}^{2}\wedge \left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge \left({X}\in {r}\wedge {r}\subseteq {A}\right)\right)\right)\to \left(\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)$
17 r19.41v ${⊢}\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)↔\left(\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)$
18 simpll ${⊢}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to {X}\in {b}$
19 simplr ${⊢}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to {b}\subseteq {r}$
20 simpr ${⊢}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to {r}\subseteq {A}$
21 19 20 sstrd ${⊢}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to {b}\subseteq {A}$
22 18 21 jca ${⊢}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to \left({X}\in {b}\wedge {b}\subseteq {A}\right)$
23 22 reximi ${⊢}\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left(\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)$
24 17 23 sylbir ${⊢}\left(\exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {r}\right)\wedge {r}\subseteq {A}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)$
25 16 24 syl ${⊢}\left({X}\in {ℝ}^{2}\wedge \left({r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\wedge \left({X}\in {r}\wedge {r}\subseteq {A}\right)\right)\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)$
26 25 rexlimdvaa ${⊢}{X}\in {ℝ}^{2}\to \left(\exists {r}\in \mathrm{ran}\left({e}\in \mathrm{ran}\left(.\right),{f}\in \mathrm{ran}\left(.\right)⟼{e}×{f}\right)\phantom{\rule{.4em}{0ex}}\left({X}\in {r}\wedge {r}\subseteq {A}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)\right)$
27 7 10 26 sylc ${⊢}\left({A}\in \left({J}{×}_{t}{J}\right)\wedge {X}\in {A}\right)\to \exists {b}\in \mathrm{ran}{R}\phantom{\rule{.4em}{0ex}}\left({X}\in {b}\wedge {b}\subseteq {A}\right)$