tpr2rico - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > tpr2rico		Structured version Visualization version GIF version

Theorem tpr2rico 34170

Description: For any point of an open set of the usual topology on (ℝ × ℝ) 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 (𝑙↑+∞) norm 𝑋. (Contributed by Thierry Arnoux, 21-Sep-2017.)

**Hypotheses**
Ref	Expression
tpr2rico.0	⊢ 𝐽 = (topGen‘ran (,))
tpr2rico.1	⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
tpr2rico.2	⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))

**Assertion**
Ref	Expression
tpr2rico	⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))

Distinct variable groups: 𝑣,𝑢,𝑥,𝑦 𝑥,𝑟,𝐴 𝐵,𝑟 𝑥,𝐺 𝑥,𝐽 𝑥,𝑋 𝑦,𝑟,𝑋 Allowed substitution hints: 𝐴(𝑦,𝑣,𝑢) 𝐵(𝑥,𝑦,𝑣,𝑢) 𝐺(𝑦,𝑣,𝑢,𝑟) 𝐽(𝑦,𝑣,𝑢,𝑟) 𝑋(𝑣,𝑢)

Proof of Theorem tpr2rico Dummy variables 𝑧 𝑚 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ioo 13347	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxf 13353	. . . . . . . . 9 ⊢ (,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
3		ffn 6686	. . . . . . . . 9 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ^ → (,) Fn (ℝ^* × ℝ^*))
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (,) Fn (ℝ^* × ℝ^*))
5		elssuni 4894	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ ∪ (𝐽 ×_t 𝐽))
6		tpr2rico.0	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (topGen‘ran (,))
7		retop 24809	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) ∈ Top
8	6, 7	eqeltri 2857	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
9		uniretop 24810	. . . . . . . . . . . . . . . 16 ⊢ ℝ = ∪ (topGen‘ran (,))
10	6	unieqi 4874	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
11	9, 10	eqtr4i 2787	. . . . . . . . . . . . . . 15 ⊢ ℝ = ∪ 𝐽
12	8, 8, 11, 11	txunii 23641	. . . . . . . . . . . . . 14 ⊢ (ℝ × ℝ) = ∪ (𝐽 ×_t 𝐽)
13	5, 12	sseqtrrdi 3975	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ (ℝ × ℝ))
14	13	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐴 ⊆ (ℝ × ℝ))
15		simplr 778	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ 𝐴)
16	14, 15	sseldd 3935	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (ℝ × ℝ))
17		xp1st 7997	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (1^st ‘𝑋) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ)
19		simpr 488	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ⁺)
20	19	rpred 13031	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ)
21	20	rehalfcld 12462	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ)
22	18, 21	resubcld 11609	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
23	22	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
24	18, 21	readdcld 11205	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
25	24	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
26		fnovrn 7566	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
27	4, 23, 25, 26	syl3anc 1389	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
28		xp2nd 7998	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (2^nd ‘𝑋) ∈ ℝ)
29	16, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ)
30	29, 21	resubcld 11609	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
31	30	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
32	29, 21	readdcld 11205	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
33	32	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
34		fnovrn 7566	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
35	4, 31, 33, 34	syl3anc 1389	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
36		eqidd 2762	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_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)))))
37		xpeq1 5657	. . . . . . . . 9 ⊢ (𝑥 = (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) → (𝑥 × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦))
38	37	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑥 = (((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))) × 𝑦)))
39		xpeq2 5664	. . . . . . . . 9 ⊢ (𝑦 = (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
40	39	eqeq2d 2772	. . . . . . . 8 ⊢ (𝑦 = (((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))))))
41	38, 40	rspc2ev 3593	. . . . . . 7 ⊢ (((((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)))) = (𝑥 × 𝑦))
42	27, 35, 36, 41	syl3anc 1389	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ∃𝑥 ∈ ran (,)∃𝑦 ∈ ran (,)((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) = (𝑥 × 𝑦))
43		eqid 2761	. . . . . . 7 ⊢ (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) = (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
44		vex 3457	. . . . . . . 8 ⊢ 𝑥 ∈ V
45		vex 3457	. . . . . . . 8 ⊢ 𝑦 ∈ V
46	44, 45	xpex 7731	. . . . . . 7 ⊢ (𝑥 × 𝑦) ∈ V
47	43, 46	elrnmpo 7527	. . . . . 6 ⊢ (((((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)))) = (𝑥 × 𝑦))
48	42, 47	sylibr 236	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)))
49		tpr2rico.2	. . . . 5 ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
50	48, 49	eleqtrrdi 2872	. . . 4 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
51	50	ralrimiva 3153	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
52		xpss 5659	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (V × V)
53	52, 16	sselid 3932	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (V × V))
54	18	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ^*)
55	19	rphalfcld 13043	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ⁺)
56	18, 55	ltsubrpd 13063	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋))
57	18, 55	ltaddrpd 13064	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))
58		elioo1 13383	. . . . . . . . 9 ⊢ ((((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)))))
59	23, 25, 58	syl2anc 593	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ↔ ((1^st ‘𝑋) ∈ ℝ^* ∧ ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋) ∧ (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))))
60	54, 56, 57, 59	mpbir3and 1355	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))))
61	29	rexrd 11226	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ^*)
62	29, 55	ltsubrpd 13063	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋))
63	29, 55	ltaddrpd 13064	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))
64		elioo1 13383	. . . . . . . . 9 ⊢ ((((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)))))
65	31, 33, 64	syl2anc 593	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ↔ ((2^nd ‘𝑋) ∈ ℝ^* ∧ ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋) ∧ (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))))
66	61, 62, 63, 65	mpbir3and 1355	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))
67	60, 66	jca 519	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∧ (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
68		elxp7 8000	. . . . . 6 ⊢ (𝑋 ∈ ((((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))))))
69	53, 67, 68	sylanbrc 592	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
70	69	ralrimiva 3153	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
71		mnfle 13131	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
73		pnfge 13126	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
75		mnfxr 11233	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
76		pnfxr 11230	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
77		ioossioo 13439	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
78	75, 76, 77	mpanl12 712	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
79	72, 74, 78	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
80		ioomax 13420	. . . . . . . . . . . . . . . 16 ⊢ (-∞(,)+∞) = ℝ
81	79, 80	sseqtrdi 3974	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
82		mnfle 13131	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
84		pnfge 13126	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
86		ioossioo 13439	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
87	75, 76, 86	mpanl12 712	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
88	83, 85, 87	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
89	88, 80	sseqtrdi 3974	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
90		xpss12 5658	. . . . . . . . . . . . . . 15 ⊢ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ ∧ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (ℝ × ℝ))
91	81, 89, 90	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (ℝ × ℝ))
92	91	sselda 3934	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (ℝ × ℝ))
93	92	expcom 417	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑥 ∈ (ℝ × ℝ)))
94	93	ancld 558	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ))))
95	94	imdistanri 577	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ (𝐽 ×_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))))))
96	13	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝐴 ⊆ (ℝ × ℝ))
97		simpr1 1207	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ 𝐴)
98	96, 97	sseldd 3935	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ (ℝ × ℝ))
99	98	3anassrs 1373	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑋 ∈ (ℝ × ℝ))
100		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑥 ∈ (ℝ × ℝ))
101		simplr 778	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ⁺)
102	101	rphalfcld 13043	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑑 / 2) ∈ ℝ⁺)
103		tpr2rico.1	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
104	103	cnre2csqima 34169	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑥 ∈ (ℝ × ℝ) ∧ (𝑑 / 2) ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
105	99, 100, 102, 104	syl3anc 1389	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
106		eqid 2761	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
107	103, 6, 106	cnrehmeo 25003	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld))
108	106	cnfldtopon 24830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
109	108	toponunii 22964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
110	12, 109	hmeof1o 23812	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
111		f1of 6801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)⟶ℂ)
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺:(ℝ × ℝ)⟶ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)⟶ℂ)
114	113, 99	ffvelcdmd 7061	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑋) ∈ ℂ)
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐺:(ℝ × ℝ)⟶ℂ)
116	115	ffvelcdmda 7060	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ ℂ)
117		sqsscirc2 34167	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) ∧ 𝑑 ∈ ℝ⁺) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
118	114, 116, 101, 117	syl21anc 848	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
119	118	imp 410	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
120	101	rpxrd 13032	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ^*)
121	120	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → 𝑑 ∈ ℝ^*)
122		cnxmet 24820	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
123	121, 122	jctil 527	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*))
124	114	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑋) ∈ ℂ)
125	116	adantr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ℂ)
126	124, 125	jca 519	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ))
127		eqid 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
128	127	cnmetdval 24818	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑋) ∈ ℂ) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
129	125, 124, 128	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
130		simpr 488	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
131	129, 130	eqbrtrd 5119	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑)
132		elbl3 24440	. . . . . . . . . . . . . . . . 17 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ↔ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑))
133	132	biimpar 481	. . . . . . . . . . . . . . . 16 ⊢ (((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) ∧ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
134	123, 126, 131, 133	syl21anc 848	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
135	119, 134	syldan 600	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
136	135	ex 416	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
137	105, 136	syld 47	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
138		f1ocnv 6814	. . . . . . . . . . . . . . 15 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ))
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)
140		f1ofun 6803	. . . . . . . . . . . . . 14 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → Fun ^◡𝐺)
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun ^◡𝐺
142		f1odm 6805	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → dom ^◡𝐺 = ℂ)
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ^◡𝐺 = ℂ
144	116, 143	eleqtrrdi 2872	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ dom ^◡𝐺)
145		funfvima 7209	. . . . . . . . . . . . 13 ⊢ ((Fun ^◡𝐺 ∧ (𝐺‘𝑥) ∈ dom ^◡𝐺) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
146	141, 144, 145	sylancr 596	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
147	107, 110	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
148		f1ocnvfv1 7255	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
149	147, 100, 148	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
150	149	eleq1d 2846	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ↔ 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
151	150	biimpd 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
152	137, 146, 151	3syld 60	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
153	152	imp 410	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
154	95, 153	syl 17	. . . . . . . . 9 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
155	154	ex 416	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
156	155	ssrdv 3940	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
157	156	ralrimiva 3153	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
158	103	mpofun 7515	. . . . . . . . . 10 ⊢ Fun 𝐺
159	158	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺)
160	13	sselda 3934	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ × ℝ))
161		f1odm 6805	. . . . . . . . . . 11 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → dom 𝐺 = (ℝ × ℝ))
162	107, 110, 161	mp2b 10	. . . . . . . . . 10 ⊢ dom 𝐺 = (ℝ × ℝ)
163	160, 162	eleqtrrdi 2872	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺)
164		simpr 488	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
165		funfvima 7209	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ 𝐴 → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴)))
166	165	imp 410	. . . . . . . . 9 ⊢ (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
167	159, 163, 164, 166	syl21anc 848	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
168		hmeoima 23813	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) ∧ 𝐴 ∈ (𝐽 ×_t 𝐽)) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
169	107, 168	mpan 700	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
170	106	cnfldtopn 24829	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
171	170	elmopn2 24493	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∈ (∞Met‘ℂ) → ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))))
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
173	172	simprbi 501	. . . . . . . . . 10 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
174	169, 173	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
175	174	adantr 484	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
176		oveq1 7398	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑋) → (𝑚(ball‘(abs ∘ − ))𝑑) = ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
177	176	sseq1d 3965	. . . . . . . . . 10 ⊢ (𝑚 = (𝐺‘𝑋) → ((𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
178	177	rexbidv 3185	. . . . . . . . 9 ⊢ (𝑚 = (𝐺‘𝑋) → (∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
179	178	rspcva 3578	. . . . . . . 8 ⊢ (((𝐺‘𝑋) ∈ (𝐺 “ 𝐴) ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
180	167, 175, 179	syl2anc 593	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
181		imass2 6087	. . . . . . . . . 10 ⊢ (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)))
182		f1of1 6800	. . . . . . . . . . . . 13 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–1-1→ℂ)
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12 ⊢ 𝐺:(ℝ × ℝ)–1-1→ℂ
184		f1imacnv 6818	. . . . . . . . . . . 12 ⊢ ((𝐺:(ℝ × ℝ)–1-1→ℂ ∧ 𝐴 ⊆ (ℝ × ℝ)) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
185	183, 13, 184	sylancr 596	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
186	185	sseq2d 3966	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ((^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)) ↔ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
187	181, 186	imbitrid 246	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
188	187	reximdv 3176	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
189	188	adantr 484	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
190	180, 189	mpd 15	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴)
191		r19.29 3124	. . . . . 6 ⊢ ((∀𝑑 ∈ ℝ⁺ ((((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 593	. . . . 5 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ∧ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
193		sstr 3942	. . . . . 6 ⊢ ((((((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 3099	. . . . 5 ⊢ (∃𝑑 ∈ ℝ⁺ (((((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 17	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ 𝐴)
196		r19.29 3124	. . . 4 ⊢ ((∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((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	70, 195, 196	syl2anc 593	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_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 3124	. . 3 ⊢ ((∀𝑑 ∈ ℝ⁺ ((((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	51, 197, 198	syl2anc 593	. 2 ⊢ ((𝐴 ∈ (𝐽 ×_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 2850	. . . . 5 ⊢ (𝑟 = ((((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 3959	. . . . 5 ⊢ (𝑟 = ((((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 641	. . . 4 ⊢ (𝑟 = ((((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 3580	. . 3 ⊢ ((((((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 3158	. 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)))) ⊆ 𝐴)) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))
205	199, 204	syl 17	1 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ∀wral 3075 ∃wrex 3085 Vcvv 3453 ⊆ wss 3902 𝒫 cpw 4552 ∪ cuni 4862 class class class wbr 5097 × cxp 5641 ^◡ccnv 5642 dom cdm 5643 ran crn 5644 “ cima 5646 ∘ ccom 5647 Fun wfun 6510 Fn wfn 6511 ⟶wf 6512 –1-1→wf1 6513 –1-1-onto→wf1o 6515 ‘cfv 6516 (class class class)co 7391 ∈ cmpo 7393 1^st c1st 7963 2^nd c2nd 7964 ℂcc 11065 ℝcr 11066 ici 11069 + caddc 11070 · cmul 11072 +∞cpnf 11207 -∞cmnf 11208 ℝ^*cxr 11209 < clt 11210 ≤ cle 11211 − cmin 11408 / cdiv 11838 2c2 12266 ℝ⁺crp 12987 (,)cioo 13343 ℜcre 15115 ℑcim 15116 abscabs 15252 TopOpenctopn 17441 topGenctg 17457 ∞Metcxmet 21397 ballcbl 21399 ℂ_fldccnfld 21412 Topctop 22941 ×_t ctx 23608 Homeochmeo 23801

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145 ax-addf 11146

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-se 5597 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-isom 6525 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-supp 8135 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-ixp 8874 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-fsupp 9302 df-fi 9351 df-sup 9382 df-inf 9383 df-oi 9452 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-7 12279 df-8 12280 df-9 12281 df-n0 12476 df-z 12563 df-dec 12683 df-uz 12834 df-q 12944 df-rp 12988 df-xneg 13108 df-xadd 13109 df-xmul 13110 df-ioo 13347 df-icc 13350 df-fz 13507 df-fzo 13654 df-seq 14009 df-exp 14069 df-hash 14338 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-starv 17292 df-sca 17293 df-vsca 17294 df-ip 17295 df-tset 17296 df-ple 17297 df-ds 17299 df-unif 17300 df-hom 17301 df-cco 17302 df-rest 17442 df-topn 17443 df-0g 17461 df-gsum 17462 df-topgen 17463 df-pt 17464 df-prds 17467 df-xrs 17523 df-qtop 17528 df-imas 17529 df-xps 17531 df-mre 17605 df-mrc 17606 df-acs 17608 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-mulg 19101 df-cntz 19348 df-cmn 19813 df-psmet 21404 df-xmet 21405 df-met 21406 df-bl 21407 df-mopn 21408 df-cnfld 21413 df-top 22942 df-topon 22959 df-topsp 22981 df-bases 22994 df-cn 23275 df-cnp 23276 df-tx 23610 df-hmeo 23803 df-xms 24368 df-ms 24369 df-tms 24370 df-cncf 24928

This theorem is referenced by: dya2iocnei 34540

W3C validator