tpr2rico

Description: For any point of an open set of the usual topology on ( RR X. RR ) there is an open square which contains that point and is entirely in the open set. This is square is actually a ball by the ( l ^ +oo ) norm X . (Contributed by Thierry Arnoux, 21-Sep-2017)

	Ref	Expression
Hypotheses	tpr2rico.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
	tpr2rico.1	⊢ 𝐺 = ( 𝑢 ∈ ℝ , 𝑣 ∈ ℝ ↦ ( 𝑢 + ( i · 𝑣 ) ) )
	tpr2rico.2	⊢ 𝐵 = ran ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) )
Assertion	tpr2rico	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		tpr2rico.0	⊢ 𝐽 = ( topGen ‘ ran (,) )
2		tpr2rico.1	⊢ 𝐺 = ( 𝑢 ∈ ℝ , 𝑣 ∈ ℝ ↦ ( 𝑢 + ( i · 𝑣 ) ) )
3		tpr2rico.2	⊢ 𝐵 = ran ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) )
4		df-ioo	⊢ (,) = ( 𝑥 ∈ ℝ^* , 𝑦 ∈ ℝ^* ↦ { 𝑧 ∈ ℝ^* ∣ ( 𝑥 < 𝑧 ∧ 𝑧 < 𝑦 ) } )
5	4	ixxf	⊢ (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^*
6		ffn	⊢ ( (,) : ( ℝ^* × ℝ^* ) ⟶ 𝒫 ℝ^* → (,) Fn ( ℝ^* × ℝ^* ) )
7	5 6	mp1i	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → (,) Fn ( ℝ^* × ℝ^* ) )
8		elssuni	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → 𝐴 ⊆ ∪ ( 𝐽 ×_t 𝐽 ) )
9		retop	⊢ ( topGen ‘ ran (,) ) ∈ Top
10	1 9	eqeltri	⊢ 𝐽 ∈ Top
11		uniretop	⊢ ℝ = ∪ ( topGen ‘ ran (,) )
12	1	unieqi	⊢ ∪ 𝐽 = ∪ ( topGen ‘ ran (,) )
13	11 12	eqtr4i	⊢ ℝ = ∪ 𝐽
14	10 10 13 13	txunii	⊢ ( ℝ × ℝ ) = ∪ ( 𝐽 ×_t 𝐽 )
15	8 14	sseqtrrdi	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → 𝐴 ⊆ ( ℝ × ℝ ) )
16	15	ad2antrr	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝐴 ⊆ ( ℝ × ℝ ) )
17		simplr	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑋 ∈ 𝐴 )
18	16 17	sseldd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑋 ∈ ( ℝ × ℝ ) )
19		xp1st	⊢ ( 𝑋 ∈ ( ℝ × ℝ ) → ( 1^st ‘ 𝑋 ) ∈ ℝ )
20	18 19	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 1^st ‘ 𝑋 ) ∈ ℝ )
21		simpr	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑑 ∈ ℝ⁺ )
22	21	rpred	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑑 ∈ ℝ )
23	22	rehalfcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 𝑑 / 2 ) ∈ ℝ )
24	20 23	resubcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ )
25	24	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* )
26	20 23	readdcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ )
27	26	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* )
28		fnovrn	⊢ ( ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* ∧ ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) )
29	7 25 27 28	syl3anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) )
30		xp2nd	⊢ ( 𝑋 ∈ ( ℝ × ℝ ) → ( 2^nd ‘ 𝑋 ) ∈ ℝ )
31	18 30	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 2^nd ‘ 𝑋 ) ∈ ℝ )
32	31 23	resubcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ )
33	32	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* )
34	31 23	readdcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ )
35	34	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* )
36		fnovrn	⊢ ( ( (,) Fn ( ℝ^* × ℝ^* ) ∧ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* ∧ ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) )
37	7 33 35 36	syl3anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) )
38		eqidd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
39		xpeq1	⊢ ( 𝑥 = ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) → ( 𝑥 × 𝑦 ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × 𝑦 ) )
40	39	eqeq2d	⊢ ( 𝑥 = ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) → ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( 𝑥 × 𝑦 ) ↔ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × 𝑦 ) ) )
41		xpeq2	⊢ ( 𝑦 = ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × 𝑦 ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
42	41	eqeq2d	⊢ ( 𝑦 = ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) → ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × 𝑦 ) ↔ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) )
43	40 42	rspc2ev	⊢ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) ∧ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∈ ran (,) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) → ∃ 𝑥 ∈ ran (,) ∃ 𝑦 ∈ ran (,) ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( 𝑥 × 𝑦 ) )
44	29 37 38 43	syl3anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ∃ 𝑥 ∈ ran (,) ∃ 𝑦 ∈ ran (,) ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( 𝑥 × 𝑦 ) )
45		eqid	⊢ ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) ) = ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) )
46		vex	⊢ 𝑥 ∈ V
47		vex	⊢ 𝑦 ∈ V
48	46 47	xpex	⊢ ( 𝑥 × 𝑦 ) ∈ V
49	45 48	elrnmpo	⊢ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ ran ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) ) ↔ ∃ 𝑥 ∈ ran (,) ∃ 𝑦 ∈ ran (,) ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) = ( 𝑥 × 𝑦 ) )
50	44 49	sylibr	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ ran ( 𝑥 ∈ ran (,) , 𝑦 ∈ ran (,) ↦ ( 𝑥 × 𝑦 ) ) )
51	50 3	eleqtrrdi	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 )
52	51	ralrimiva	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 )
53		xpss	⊢ ( ℝ × ℝ ) ⊆ ( V × V )
54	53 18	sseldi	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑋 ∈ ( V × V ) )
55	20	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 1^st ‘ 𝑋 ) ∈ ℝ^* )
56	21	rphalfcld	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 𝑑 / 2 ) ∈ ℝ⁺ )
57	20 56	ltsubrpd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 1^st ‘ 𝑋 ) )
58	20 56	ltaddrpd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 1^st ‘ 𝑋 ) < ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) )
59		elioo1	⊢ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* ∧ ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* ) → ( ( 1^st ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ↔ ( ( 1^st ‘ 𝑋 ) ∈ ℝ^* ∧ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 1^st ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑋 ) < ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
60	25 27 59	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ↔ ( ( 1^st ‘ 𝑋 ) ∈ ℝ^* ∧ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 1^st ‘ 𝑋 ) ∧ ( 1^st ‘ 𝑋 ) < ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
61	55 57 58 60	mpbir3and	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 1^st ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) )
62	31	rexrd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 2^nd ‘ 𝑋 ) ∈ ℝ^* )
63	31 56	ltsubrpd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 2^nd ‘ 𝑋 ) )
64	31 56	ltaddrpd	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 2^nd ‘ 𝑋 ) < ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) )
65		elioo1	⊢ ( ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* ∧ ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* ) → ( ( 2^nd ‘ 𝑋 ) ∈ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ↔ ( ( 2^nd ‘ 𝑋 ) ∈ ℝ^* ∧ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 2^nd ‘ 𝑋 ) ∧ ( 2^nd ‘ 𝑋 ) < ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
66	33 35 65	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) ∈ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ↔ ( ( 2^nd ‘ 𝑋 ) ∈ ℝ^* ∧ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) < ( 2^nd ‘ 𝑋 ) ∧ ( 2^nd ‘ 𝑋 ) < ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
67	62 63 64 66	mpbir3and	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 2^nd ‘ 𝑋 ) ∈ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) )
68	61 67	jca	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
69		elxp7	⊢ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ↔ ( 𝑋 ∈ ( V × V ) ∧ ( ( 1^st ‘ 𝑋 ) ∈ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ∧ ( 2^nd ‘ 𝑋 ) ∈ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) )
70	54 68 69	sylanbrc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
71	70	ralrimiva	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑑 ∈ ℝ⁺ 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) )
72		mnfle	⊢ ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* → -∞ ≤ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) )
73	25 72	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → -∞ ≤ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) )
74		pnfge	⊢ ( ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* → ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ )
75	27 74	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ )
76		mnfxr	⊢ -∞ ∈ ℝ^*
77		pnfxr	⊢ +∞ ∈ ℝ^*
78		ioossioo	⊢ ( ( ( -∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) ∧ ( -∞ ≤ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∧ ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ ) ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
79	76 77 78	mpanl12	⊢ ( ( -∞ ≤ ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∧ ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
80	73 75 79	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
81		ioomax	⊢ ( -∞ (,) +∞ ) = ℝ
82	80 81	sseqtrdi	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ℝ )
83		mnfle	⊢ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∈ ℝ^* → -∞ ≤ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) )
84	33 83	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → -∞ ≤ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) )
85		pnfge	⊢ ( ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ∈ ℝ^* → ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ )
86	35 85	syl	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ )
87		ioossioo	⊢ ( ( ( -∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^* ) ∧ ( -∞ ≤ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∧ ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ ) ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
88	76 77 87	mpanl12	⊢ ( ( -∞ ≤ ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) ∧ ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ≤ +∞ ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
89	84 86 88	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ( -∞ (,) +∞ ) )
90	89 81	sseqtrdi	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ℝ )
91		xpss12	⊢ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ℝ ∧ ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ⊆ ℝ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ℝ × ℝ ) )
92	82 90 91	syl2anc	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ℝ × ℝ ) )
93	92	sselda	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) → 𝑥 ∈ ( ℝ × ℝ ) )
94	93	expcom	⊢ ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝑥 ∈ ( ℝ × ℝ ) ) )
95	94	ancld	⊢ ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ) )
96	95	imdistanri	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) → ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) )
97	15	adantr	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ) → 𝐴 ⊆ ( ℝ × ℝ ) )
98		simpr1	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ) → 𝑋 ∈ 𝐴 )
99	97 98	sseldd	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ) → 𝑋 ∈ ( ℝ × ℝ ) )
100	99	3anassrs	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝑋 ∈ ( ℝ × ℝ ) )
101		simpr	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝑥 ∈ ( ℝ × ℝ ) )
102		simplr	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝑑 ∈ ℝ⁺ )
103	102	rphalfcld	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝑑 / 2 ) ∈ ℝ⁺ )
104	2	cnre2csqima	⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ∧ ( 𝑑 / 2 ) ∈ ℝ⁺ ) → ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) ) )
105	100 101 103 104	syl3anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) ) )
106		eqid	⊢ ( TopOpen ‘ ℂ_fld ) = ( TopOpen ‘ ℂ_fld )
107	2 1 106	cnrehmeo	⊢ 𝐺 ∈ ( ( 𝐽 ×_t 𝐽 ) Homeo ( TopOpen ‘ ℂ_fld ) )
108	106	cnfldtopon	⊢ ( TopOpen ‘ ℂ_fld ) ∈ ( TopOn ‘ ℂ )
109	108	toponunii	⊢ ℂ = ∪ ( TopOpen ‘ ℂ_fld )
110	14 109	hmeof1o	⊢ ( 𝐺 ∈ ( ( 𝐽 ×_t 𝐽 ) Homeo ( TopOpen ‘ ℂ_fld ) ) → 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ )
111		f1of	⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐺 : ( ℝ × ℝ ) ⟶ ℂ )
112	107 110 111	mp2b	⊢ 𝐺 : ( ℝ × ℝ ) ⟶ ℂ
113	112	a1i	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝐺 : ( ℝ × ℝ ) ⟶ ℂ )
114	113 100	ffvelrnd	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
115	112	a1i	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → 𝐺 : ( ℝ × ℝ ) ⟶ ℂ )
116	115	ffvelrnda	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
117		sqsscirc2	⊢ ( ( ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) )
118	114 116 102 117	syl21anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) )
119	118	imp	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 )
120	102	rpxrd	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝑑 ∈ ℝ^* )
121	120	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → 𝑑 ∈ ℝ^* )
122		cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
123	121 122	jctil	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑑 ∈ ℝ^* ) )
124	114	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
125	116	adantr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
126	124 125	jca	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) )
127		eqid	⊢ ( abs ∘ − ) = ( abs ∘ − )
128	127	cnmetdval	⊢ ( ( ( 𝐺 ‘ 𝑥 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑋 ) ∈ ℂ ) → ( ( 𝐺 ‘ 𝑥 ) ( abs ∘ − ) ( 𝐺 ‘ 𝑋 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) )
129	125 124 128	syl2anc	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( ( 𝐺 ‘ 𝑥 ) ( abs ∘ − ) ( 𝐺 ‘ 𝑋 ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) )
130		simpr	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 )
131	129 130	eqbrtrd	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( ( 𝐺 ‘ 𝑥 ) ( abs ∘ − ) ( 𝐺 ‘ 𝑋 ) ) < 𝑑 )
132		elbl3	⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑑 ∈ ℝ^* ) ∧ ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ↔ ( ( 𝐺 ‘ 𝑥 ) ( abs ∘ − ) ( 𝐺 ‘ 𝑋 ) ) < 𝑑 ) )
133	132	biimpar	⊢ ( ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑑 ∈ ℝ^* ) ∧ ( ( 𝐺 ‘ 𝑋 ) ∈ ℂ ∧ ( 𝐺 ‘ 𝑥 ) ∈ ℂ ) ) ∧ ( ( 𝐺 ‘ 𝑥 ) ( abs ∘ − ) ( 𝐺 ‘ 𝑋 ) ) < 𝑑 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
134	123 126 131 133	syl21anc	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( abs ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) < 𝑑 ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
135	119 134	syldan	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
136	135	ex	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ( ( abs ‘ ( ℜ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ∧ ( abs ‘ ( ℑ ‘ ( ( 𝐺 ‘ 𝑥 ) − ( 𝐺 ‘ 𝑋 ) ) ) ) < ( 𝑑 / 2 ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
137	105 136	syld	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
138		f1ocnv	⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → ^◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ ) )
139	107 110 138	mp2b	⊢ ^◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ )
140		f1ofun	⊢ ( ^◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ ) → Fun ^◡ 𝐺 )
141	139 140	ax-mp	⊢ Fun ^◡ 𝐺
142		f1odm	⊢ ( ^◡ 𝐺 : ℂ –1-1-onto→ ( ℝ × ℝ ) → dom ^◡ 𝐺 = ℂ )
143	139 142	ax-mp	⊢ dom ^◡ 𝐺 = ℂ
144	116 143	eleqtrrdi	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝐺 ‘ 𝑥 ) ∈ dom ^◡ 𝐺 )
145		funfvima	⊢ ( ( Fun ^◡ 𝐺 ∧ ( 𝐺 ‘ 𝑥 ) ∈ dom ^◡ 𝐺 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
146	141 144 145	sylancr	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ( 𝐺 ‘ 𝑥 ) ∈ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
147	107 110	mp1i	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ )
148		f1ocnvfv1	⊢ ( ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) = 𝑥 )
149	147 101 148	syl2anc	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) = 𝑥 )
150	149	eleq1d	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ↔ 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
151	150	biimpd	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( ( ^◡ 𝐺 ‘ ( 𝐺 ‘ 𝑥 ) ) ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) → 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
152	137 146 151	3syld	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) → ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
153	152	imp	⊢ ( ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ℝ × ℝ ) ) ∧ 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) → 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
154	96 153	syl	⊢ ( ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) ∧ 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) → 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
155	154	ex	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( 𝑥 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → 𝑥 ∈ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ) )
156	155	ssrdv	⊢ ( ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑑 ∈ ℝ⁺ ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
157	156	ralrimiva	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) )
158	2	mpofun	⊢ Fun 𝐺
159	158	a1i	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → Fun 𝐺 )
160	15	sselda	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ℝ × ℝ ) )
161		f1odm	⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → dom 𝐺 = ( ℝ × ℝ ) )
162	107 110 161	mp2b	⊢ dom 𝐺 = ( ℝ × ℝ )
163	160 162	eleqtrrdi	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ dom 𝐺 )
164		simpr	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
165		funfvima	⊢ ( ( Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺 ) → ( 𝑋 ∈ 𝐴 → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 “ 𝐴 ) ) )
166	165	imp	⊢ ( ( ( Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 “ 𝐴 ) )
167	159 163 164 166	syl21anc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 “ 𝐴 ) )
168		hmeoima	⊢ ( ( 𝐺 ∈ ( ( 𝐽 ×_t 𝐽 ) Homeo ( TopOpen ‘ ℂ_fld ) ) ∧ 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ) → ( 𝐺 “ 𝐴 ) ∈ ( TopOpen ‘ ℂ_fld ) )
169	107 168	mpan	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ( 𝐺 “ 𝐴 ) ∈ ( TopOpen ‘ ℂ_fld ) )
170	106	cnfldtopn	⊢ ( TopOpen ‘ ℂ_fld ) = ( MetOpen ‘ ( abs ∘ − ) )
171	170	elmopn2	⊢ ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) → ( ( 𝐺 “ 𝐴 ) ∈ ( TopOpen ‘ ℂ_fld ) ↔ ( ( 𝐺 “ 𝐴 ) ⊆ ℂ ∧ ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ) ) )
172	122 171	ax-mp	⊢ ( ( 𝐺 “ 𝐴 ) ∈ ( TopOpen ‘ ℂ_fld ) ↔ ( ( 𝐺 “ 𝐴 ) ⊆ ℂ ∧ ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ) )
173	172	simprbi	⊢ ( ( 𝐺 “ 𝐴 ) ∈ ( TopOpen ‘ ℂ_fld ) → ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) )
174	169 173	syl	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) )
175	174	adantr	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) )
176		oveq1	⊢ ( 𝑚 = ( 𝐺 ‘ 𝑋 ) → ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) = ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) )
177	176	sseq1d	⊢ ( 𝑚 = ( 𝐺 ‘ 𝑋 ) → ( ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ↔ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ) )
178	177	rexbidv	⊢ ( 𝑚 = ( 𝐺 ‘ 𝑋 ) → ( ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ↔ ∃ 𝑑 ∈ ℝ⁺ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ) )
179	178	rspcva	⊢ ( ( ( 𝐺 ‘ 𝑋 ) ∈ ( 𝐺 “ 𝐴 ) ∧ ∀ 𝑚 ∈ ( 𝐺 “ 𝐴 ) ∃ 𝑑 ∈ ℝ⁺ ( 𝑚 ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) ) → ∃ 𝑑 ∈ ℝ⁺ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) )
180	167 175 179	syl2anc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) )
181		imass2	⊢ ( ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) → ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ ( ^◡ 𝐺 “ ( 𝐺 “ 𝐴 ) ) )
182		f1of1	⊢ ( 𝐺 : ( ℝ × ℝ ) –1-1-onto→ ℂ → 𝐺 : ( ℝ × ℝ ) –1-1→ ℂ )
183	107 110 182	mp2b	⊢ 𝐺 : ( ℝ × ℝ ) –1-1→ ℂ
184		f1imacnv	⊢ ( ( 𝐺 : ( ℝ × ℝ ) –1-1→ ℂ ∧ 𝐴 ⊆ ( ℝ × ℝ ) ) → ( ^◡ 𝐺 “ ( 𝐺 “ 𝐴 ) ) = 𝐴 )
185	183 15 184	sylancr	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ( ^◡ 𝐺 “ ( 𝐺 “ 𝐴 ) ) = 𝐴 )
186	185	sseq2d	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ( ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ ( ^◡ 𝐺 “ ( 𝐺 “ 𝐴 ) ) ↔ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
187	181 186	syl5ib	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ( ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) → ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
188	187	reximdv	⊢ ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) → ( ∃ 𝑑 ∈ ℝ⁺ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
189	188	adantr	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑑 ∈ ℝ⁺ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ⊆ ( 𝐺 “ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
190	180 189	mpd	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 )
191		r19.29	⊢ ( ( ∀ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ∃ 𝑑 ∈ ℝ⁺ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
192	157 190 191	syl2anc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) )
193		sstr	⊢ ( ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) → ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 )
194	193	reximi	⊢ ( ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ∧ ( ^◡ 𝐺 “ ( ( 𝐺 ‘ 𝑋 ) ( ball ‘ ( abs ∘ − ) ) 𝑑 ) ) ⊆ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 )
195	192 194	syl	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 )
196		r19.29	⊢ ( ( ∀ 𝑑 ∈ ℝ⁺ 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) )
197	71 195 196	syl2anc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) )
198		r19.29	⊢ ( ( ∀ 𝑑 ∈ ℝ⁺ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 ∧ ∃ 𝑑 ∈ ℝ⁺ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 ∧ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) )
199	52 197 198	syl2anc	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 ∧ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) )
200		eleq2	⊢ ( 𝑟 = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( 𝑋 ∈ 𝑟 ↔ 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ) )
201		sseq1	⊢ ( 𝑟 = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( 𝑟 ⊆ 𝐴 ↔ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) )
202	200 201	anbi12d	⊢ ( 𝑟 = ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) → ( ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) ↔ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) )
203	202	rspcev	⊢ ( ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 ∧ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) )
204	203	rexlimivw	⊢ ( ∃ 𝑑 ∈ ℝ⁺ ( ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∈ 𝐵 ∧ ( 𝑋 ∈ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ∧ ( ( ( ( 1^st ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 1^st ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) × ( ( ( 2^nd ‘ 𝑋 ) − ( 𝑑 / 2 ) ) (,) ( ( 2^nd ‘ 𝑋 ) + ( 𝑑 / 2 ) ) ) ) ⊆ 𝐴 ) ) → ∃ 𝑟 ∈ 𝐵 ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) )
205	199 204	syl	⊢ ( ( 𝐴 ∈ ( 𝐽 ×_t 𝐽 ) ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑟 ∈ 𝐵 ( 𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴 ) )

Metamath Proof Explorer

Theorem tpr2rico

Proof