Theorem 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	⊢ 𝐽 = ( topGen ‘ ran (,) )
	dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
Assertion	dya2icoseg2	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3		eqid	⊢ ( ⌊ ‘ ( 1 − ( 2 logb 𝑑 ) ) ) = ( ⌊ ‘ ( 1 − ( 2 logb 𝑑 ) ) )
4	1 2 3	dya2icoseg	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+ ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
5	4	ralrimiva	⊢ ( 𝑋 ∈ ℝ → ∀ 𝑑 ∈ ℝ+ ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
6	5	3ad2ant1	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∀ 𝑑 ∈ ℝ+ ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) )
7		simp3	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → 𝑋 ∈ 𝐸 )
8		iooex	⊢ (,) ∈ V
9	8	rnex	⊢ ran (,) ∈ V
10		bastg	⊢ ( ran (,) ∈ V → ran (,) ⊆ ( topGen ‘ ran (,) ) )
11	9 10	ax-mp	⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
12		simp2	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → 𝐸 ∈ ran (,) )
13	11 12	sselid	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → 𝐸 ∈ ( topGen ‘ ran (,) ) )
14	13 1	eleqtrrdi	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → 𝐸 ∈ 𝐽 )
15		eqid	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
16	15	rexmet	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ )
17		recms	⊢ ℝfld ∈ CMetSp
18		cmsms	⊢ ( ℝfld ∈ CMetSp → ℝfld ∈ MetSp )
19		msxms	⊢ ( ℝfld ∈ MetSp → ℝfld ∈ ∞MetSp )
20	17 18 19	mp2b	⊢ ℝfld ∈ ∞MetSp
21		retopn	⊢ ( topGen ‘ ran (,) ) = ( TopOpen ‘ ℝfld )
22	1 21	eqtri	⊢ 𝐽 = ( TopOpen ‘ ℝfld )
23		rebase	⊢ ℝ = ( Base ‘ ℝfld )
24		reds	⊢ ( abs ∘ − ) = ( dist ‘ ℝfld )
25	24	reseq1i	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) = ( ( dist ‘ ℝfld ) ↾ ( ℝ × ℝ ) )
26	22 23 25	xmstopn	⊢ ( ℝfld ∈ ∞MetSp → 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) )
27	20 26	ax-mp	⊢ 𝐽 = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) )
28	27	elmopn2	⊢ ( ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( ∞Met ‘ ℝ ) → ( 𝐸 ∈ 𝐽 ↔ ( 𝐸 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐸 ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ) ) )
29	16 28	ax-mp	⊢ ( 𝐸 ∈ 𝐽 ↔ ( 𝐸 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝐸 ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ) )
30	29	simprbi	⊢ ( 𝐸 ∈ 𝐽 → ∀ 𝑥 ∈ 𝐸 ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 )
31	14 30	syl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∀ 𝑥 ∈ 𝐸 ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 )
32		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) = ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) )
33	32	sseq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ) )
34	33	rexbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ∃ 𝑑 ∈ ℝ+ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ) )
35	34	rspcva	⊢ ( ( 𝑋 ∈ 𝐸 ∧ ∀ 𝑥 ∈ 𝐸 ∃ 𝑑 ∈ ℝ+ ( 𝑥 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ) → ∃ 𝑑 ∈ ℝ+ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 )
36	7 31 35	syl2anc	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∃ 𝑑 ∈ ℝ+ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 )
37		rpre	⊢ ( 𝑑 ∈ ℝ+ → 𝑑 ∈ ℝ )
38	15	bl2ioo	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) = ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) )
39	38	sseq1d	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ ) → ( ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
40	37 39	sylan2	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝑑 ∈ ℝ+ ) → ( ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
41	40	rexbidva	⊢ ( 𝑋 ∈ ℝ → ( ∃ 𝑑 ∈ ℝ+ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ∃ 𝑑 ∈ ℝ+ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
42	41	3ad2ant1	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ( ∃ 𝑑 ∈ ℝ+ ( 𝑋 ( ball ‘ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ) 𝑑 ) ⊆ 𝐸 ↔ ∃ 𝑑 ∈ ℝ+ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
43	36 42	mpbid	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∃ 𝑑 ∈ ℝ+ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 )
44		r19.29	⊢ ( ( ∀ 𝑑 ∈ ℝ+ ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ∃ 𝑑 ∈ ℝ+ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → ∃ 𝑑 ∈ ℝ+ ( ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
45	6 43 44	syl2anc	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∃ 𝑑 ∈ ℝ+ ( ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
46		r19.41v	⊢ ( ∃ 𝑏 ∈ ran 𝐼 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) ↔ ( ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) )
47		sstr	⊢ ( ( 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → 𝑏 ⊆ 𝐸 )
48	47	anim2i	⊢ ( ( 𝑋 ∈ 𝑏 ∧ ( 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) ) → ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )
49	48	anassrs	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )
50	49	reximi	⊢ ( ∃ 𝑏 ∈ ran 𝐼 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )
51	46 50	sylbir	⊢ ( ( ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )
52	51	rexlimivw	⊢ ( ∃ 𝑑 ∈ ℝ+ ( ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ) ∧ ( ( 𝑋 − 𝑑 ) (,) ( 𝑋 + 𝑑 ) ) ⊆ 𝐸 ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )
53	45 52	syl	⊢ ( ( 𝑋 ∈ ℝ ∧ 𝐸 ∈ ran (,) ∧ 𝑋 ∈ 𝐸 ) → ∃ 𝑏 ∈ ran 𝐼 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐸 ) )