dya2icoseg2

Description: For any point and any open interval of RR containing that point, there is a closed-below open-above dyadic rational interval which contains that point and is included in the original interval. (Contributed by Thierry Arnoux, 12-Oct-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}}))$
Assertion	dya2icoseg2	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \exists b \in ran I (X \in b \land b \subseteq E)$

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		eqid	$⊢ ⌊1 - \log_{2} d⌋ = ⌊1 - \log_{2} d⌋$
4	1 2 3	dya2icoseg	$⊢ (X \in ℝ \land d \in ℝ^{+}) \to \exists b \in ran I (X \in b \land b \subseteq (X - d, X + d))$
5	4	ralrimiva	$⊢ X \in ℝ \to \forall d \in ℝ^{+} \exists b \in ran I (X \in b \land b \subseteq (X - d, X + d))$
6	5	3ad2ant1	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \forall d \in ℝ^{+} \exists b \in ran I (X \in b \land b \subseteq (X - d, X + d))$
7		simp3	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to X \in E$
8		iooex	$⊢ (.) \in V$
9	8	rnex	$⊢ ran (.) \in V$
10		bastg	$⊢ ran (.) \in V \to ran (.) \subseteq topGen (ran (.))$
11	9 10	ax-mp	$⊢ ran (.) \subseteq topGen (ran (.))$
12		simp2	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to E \in ran (.)$
13	11 12	sselid	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to E \in topGen (ran (.))$
14	13 1	eleqtrrdi	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to E \in J$
15		eqid	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {(abs \circ -) ↾}_{ℝ^{2}}$
16	15	rexmet	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ)$
17		recms	$⊢ ℝ_{fld} \in CMetSp$
18		cmsms	$⊢ ℝ_{fld} \in CMetSp \to ℝ_{fld} \in MetSp$
19		msxms	$⊢ ℝ_{fld} \in MetSp \to ℝ_{fld} \in ∞MetSp$
20	17 18 19	mp2b	$⊢ ℝ_{fld} \in ∞MetSp$
21		retopn	$⊢ topGen (ran (.)) = TopOpen (ℝ_{fld})$
22	1 21	eqtri	$⊢ J = TopOpen (ℝ_{fld})$
23		rebase	$⊢ ℝ = {Base}_{ℝ_{fld}}$
24		reds	$⊢ abs \circ - = dist (ℝ_{fld})$
25	24	reseq1i	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} = {dist (ℝ_{fld}) ↾}_{ℝ^{2}}$
26	22 23 25	xmstopn	$⊢ ℝ_{fld} \in ∞MetSp \to J = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
27	20 26	ax-mp	$⊢ J = MetOpen ({(abs \circ -) ↾}_{ℝ^{2}})$
28	27	elmopn2	$⊢ {(abs \circ -) ↾}_{ℝ^{2}} \in ∞Met (ℝ) \to (E \in J \leftrightarrow (E \subseteq ℝ \land \forall x \in E \exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E))$
29	16 28	ax-mp	$⊢ E \in J \leftrightarrow (E \subseteq ℝ \land \forall x \in E \exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E)$
30	29	simprbi	$⊢ E \in J \to \forall x \in E \exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E$
31	14 30	syl	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \forall x \in E \exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E$
32		oveq1	$⊢ x = X \to x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d = X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d$
33	32	sseq1d	$⊢ x = X \to (x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E)$
34	33	rexbidv	$⊢ x = X \to (\exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow \exists d \in ℝ^{+} X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E)$
35	34	rspcva	$⊢ (X \in E \land \forall x \in E \exists d \in ℝ^{+} x ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E) \to \exists d \in ℝ^{+} X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E$
36	7 31 35	syl2anc	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \exists d \in ℝ^{+} X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E$
37		rpre	$⊢ d \in ℝ^{+} \to d \in ℝ$
38	15	bl2ioo	$⊢ (X \in ℝ \land d \in ℝ) \to X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d = (X - d, X + d)$
39	38	sseq1d	$⊢ (X \in ℝ \land d \in ℝ) \to (X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow (X - d, X + d) \subseteq E)$
40	37 39	sylan2	$⊢ (X \in ℝ \land d \in ℝ^{+}) \to (X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow (X - d, X + d) \subseteq E)$
41	40	rexbidva	$⊢ X \in ℝ \to (\exists d \in ℝ^{+} X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow \exists d \in ℝ^{+} (X - d, X + d) \subseteq E)$
42	41	3ad2ant1	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to (\exists d \in ℝ^{+} X ball ({(abs \circ -) ↾}_{ℝ^{2}}) d \subseteq E \leftrightarrow \exists d \in ℝ^{+} (X - d, X + d) \subseteq E)$
43	36 42	mpbid	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \exists d \in ℝ^{+} (X - d, X + d) \subseteq E$
44		r19.29	$⊢ (\forall d \in ℝ^{+} \exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land \exists d \in ℝ^{+} (X - d, X + d) \subseteq E) \to \exists d \in ℝ^{+} (\exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E)$
45	6 43 44	syl2anc	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \exists d \in ℝ^{+} (\exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E)$
46		r19.41v	$⊢ \exists b \in ran I ((X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E) \leftrightarrow (\exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E)$
47		sstr	$⊢ (b \subseteq (X - d, X + d) \land (X - d, X + d) \subseteq E) \to b \subseteq E$
48	47	anim2i	$⊢ (X \in b \land (b \subseteq (X - d, X + d) \land (X - d, X + d) \subseteq E)) \to (X \in b \land b \subseteq E)$
49	48	anassrs	$⊢ ((X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E) \to (X \in b \land b \subseteq E)$
50	49	reximi	$⊢ \exists b \in ran I ((X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E) \to \exists b \in ran I (X \in b \land b \subseteq E)$
51	46 50	sylbir	$⊢ (\exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E) \to \exists b \in ran I (X \in b \land b \subseteq E)$
52	51	rexlimivw	$⊢ \exists d \in ℝ^{+} (\exists b \in ran I (X \in b \land b \subseteq (X - d, X + d)) \land (X - d, X + d) \subseteq E) \to \exists b \in ran I (X \in b \land b \subseteq E)$
53	45 52	syl	$⊢ (X \in ℝ \land E \in ran (.) \land X \in E) \to \exists b \in ran I (X \in b \land b \subseteq E)$

Metamath Proof Explorer

Theorem dya2icoseg2

Proof