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 = topGen (ran (.))$
	dya2ioc.1	$⊢ I = (x \in ℤ, n \in ℤ ⟼ [\frac{x}{2^{n}}, \frac{x + 1}{2^{n}}))$
	dya2ioc.2	$⊢ R = (u \in ran I, v \in ran I ⟼ u \times v)$
Assertion	dya2iocnei	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists b \in ran R (X \in b \land b \subseteq A)$

Proof

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

Metamath Proof Explorer

Theorem dya2iocnei

Proof