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	⊢ 𝐽 = ( topGen ‘ ran (,) )
	dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
	dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
Assertion	dya2iocnei	⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		sxbrsiga.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		dya2ioc.1	⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3		dya2ioc.2	⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4		elunii	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ) → 𝑋 ∈ ∪ ( 𝐽 ×t 𝐽 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ∪ ( 𝐽 ×t 𝐽 ) )
6	1	tpr2uni	⊢ ∪ ( 𝐽 ×t 𝐽 ) = ( ℝ × ℝ )
7	5 6	eleqtrdi	⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ℝ × ℝ ) )
8		eqid	⊢ ( 𝑢 ∈ ℝ , 𝑣 ∈ ℝ ↦ ( 𝑢 + ( i · 𝑣 ) ) ) = ( 𝑢 ∈ ℝ , 𝑣 ∈ ℝ ↦ ( 𝑢 + ( i · 𝑣 ) ) )
9		eqid	⊢ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) = ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) )
10	1 8 9	tpr2rico	⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) )
11		anass	⊢ ( ( ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ 𝑋 ∈ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) ↔ ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) ) )
12	1 2 3 9	dya2iocnrect	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ 𝑋 ∈ 𝑟 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) )
13	12	3expb	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ 𝑋 ∈ 𝑟 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) )
14	13	anim1i	⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ 𝑋 ∈ 𝑟 ) ) ∧ 𝑟 ⊆ 𝐴 ) → ( ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) )
15	14	anasss	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ ( ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ 𝑋 ∈ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) ) → ( ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) )
16	11 15	sylan2br	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) ) ) → ( ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) )
17		r19.41v	⊢ ( ∃ 𝑏 ∈ ran 𝑅 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) ↔ ( ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) )
18		simpll	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → 𝑋 ∈ 𝑏 )
19		simplr	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → 𝑏 ⊆ 𝑟 )
20		simpr	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → 𝑟 ⊆ 𝐴 )
21	19 20	sstrd	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → 𝑏 ⊆ 𝐴 )
22	18 21	jca	⊢ ( ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
23	22	reximi	⊢ ( ∃ 𝑏 ∈ ran 𝑅 ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
24	17 23	sylbir	⊢ ( ( ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑟 ) ∧ 𝑟 ⊆ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
25	16 24	syl	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ ( 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ∧ ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
26	25	rexlimdvaa	⊢ ( 𝑋 ∈ ( ℝ × ℝ ) → ( ∃ 𝑟 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ) )
27	7 10 26	sylc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )