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 32881

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 13325	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxf 13331	. . . . . . . . 9 ⊢ (,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
3		ffn 6715	. . . . . . . . 9 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ^ → (,) Fn (ℝ^* × ℝ^*))
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (,) Fn (ℝ^* × ℝ^*))
5		elssuni 4941	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ ∪ (𝐽 ×_t 𝐽))
6		tpr2rico.0	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (topGen‘ran (,))
7		retop 24270	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) ∈ Top
8	6, 7	eqeltri 2830	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
9		uniretop 24271	. . . . . . . . . . . . . . . 16 ⊢ ℝ = ∪ (topGen‘ran (,))
10	6	unieqi 4921	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
11	9, 10	eqtr4i 2764	. . . . . . . . . . . . . . 15 ⊢ ℝ = ∪ 𝐽
12	8, 8, 11, 11	txunii 23089	. . . . . . . . . . . . . 14 ⊢ (ℝ × ℝ) = ∪ (𝐽 ×_t 𝐽)
13	5, 12	sseqtrrdi 4033	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ (ℝ × ℝ))
14	13	ad2antrr 725	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐴 ⊆ (ℝ × ℝ))
15		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ 𝐴)
16	14, 15	sseldd 3983	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (ℝ × ℝ))
17		xp1st 8004	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (1^st ‘𝑋) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ)
19		simpr 486	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ⁺)
20	19	rpred 13013	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ)
21	20	rehalfcld 12456	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ)
22	18, 21	resubcld 11639	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
23	22	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
24	18, 21	readdcld 11240	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
25	24	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
26		fnovrn 7579	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
27	4, 23, 25, 26	syl3anc 1372	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
28		xp2nd 8005	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (2^nd ‘𝑋) ∈ ℝ)
29	16, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ)
30	29, 21	resubcld 11639	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
31	30	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
32	29, 21	readdcld 11240	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
33	32	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
34		fnovrn 7579	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
35	4, 31, 33, 34	syl3anc 1372	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
36		eqidd 2734	. . . . . . 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 5690	. . . . . . . . 9 ⊢ (𝑥 = (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) → (𝑥 × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦))
38	37	eqeq2d 2744	. . . . . . . 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 5697	. . . . . . . . 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 2744	. . . . . . . 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 3624	. . . . . . 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 1372	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ∃𝑥 ∈ ran (,)∃𝑦 ∈ ran (,)((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) = (𝑥 × 𝑦))
43		eqid 2733	. . . . . . 7 ⊢ (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) = (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
44		vex 3479	. . . . . . . 8 ⊢ 𝑥 ∈ V
45		vex 3479	. . . . . . . 8 ⊢ 𝑦 ∈ V
46	44, 45	xpex 7737	. . . . . . 7 ⊢ (𝑥 × 𝑦) ∈ V
47	43, 46	elrnmpo 7542	. . . . . 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 233	. . . . 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 2845	. . . 4 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
51	50	ralrimiva 3147	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
52		xpss 5692	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (V × V)
53	52, 16	sselid 3980	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (V × V))
54	18	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ^*)
55	19	rphalfcld 13025	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ⁺)
56	18, 55	ltsubrpd 13045	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋))
57	18, 55	ltaddrpd 13046	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))
58		elioo1 13361	. . . . . . . . 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 585	. . . . . . . 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 1343	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))))
61	29	rexrd 11261	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ^*)
62	29, 55	ltsubrpd 13045	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋))
63	29, 55	ltaddrpd 13046	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))
64		elioo1 13361	. . . . . . . . 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 585	. . . . . . . 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 1343	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))
67	60, 66	jca 513	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∧ (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
68		elxp7 8007	. . . . . 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 584	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
70	69	ralrimiva 3147	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
71		mnfle 13111	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
73		pnfge 13107	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
75		mnfxr 11268	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
76		pnfxr 11265	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
77		ioossioo 13415	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
78	75, 76, 77	mpanl12 701	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
79	72, 74, 78	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
80		ioomax 13396	. . . . . . . . . . . . . . . 16 ⊢ (-∞(,)+∞) = ℝ
81	79, 80	sseqtrdi 4032	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
82		mnfle 13111	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
84		pnfge 13107	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
86		ioossioo 13415	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
87	75, 76, 86	mpanl12 701	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
88	83, 85, 87	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
89	88, 80	sseqtrdi 4032	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
90		xpss12 5691	. . . . . . . . . . . . . . 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 585	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (ℝ × ℝ))
92	91	sselda 3982	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (ℝ × ℝ))
93	92	expcom 415	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑥 ∈ (ℝ × ℝ)))
94	93	ancld 552	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ))))
95	94	imdistanri 571	. . . . . . . . . 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 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝐴 ⊆ (ℝ × ℝ))
97		simpr1 1195	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ 𝐴)
98	96, 97	sseldd 3983	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ (ℝ × ℝ))
99	98	3anassrs 1361	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑋 ∈ (ℝ × ℝ))
100		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑥 ∈ (ℝ × ℝ))
101		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ⁺)
102	101	rphalfcld 13025	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑑 / 2) ∈ ℝ⁺)
103		tpr2rico.1	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
104	103	cnre2csqima 32880	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑥 ∈ (ℝ × ℝ) ∧ (𝑑 / 2) ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
105	99, 100, 102, 104	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
106		eqid 2733	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
107	103, 6, 106	cnrehmeo 24461	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld))
108	106	cnfldtopon 24291	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
109	108	toponunii 22410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
110	12, 109	hmeof1o 23260	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
111		f1of 6831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)⟶ℂ)
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺:(ℝ × ℝ)⟶ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)⟶ℂ)
114	113, 99	ffvelcdmd 7085	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑋) ∈ ℂ)
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐺:(ℝ × ℝ)⟶ℂ)
116	115	ffvelcdmda 7084	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ ℂ)
117		sqsscirc2 32878	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) ∧ 𝑑 ∈ ℝ⁺) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
118	114, 116, 101, 117	syl21anc 837	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
119	118	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
120	101	rpxrd 13014	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ^*)
121	120	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → 𝑑 ∈ ℝ^*)
122		cnxmet 24281	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
123	121, 122	jctil 521	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*))
124	114	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑋) ∈ ℂ)
125	116	adantr 482	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ℂ)
126	124, 125	jca 513	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ))
127		eqid 2733	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
128	127	cnmetdval 24279	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑋) ∈ ℂ) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
129	125, 124, 128	syl2anc 585	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
130		simpr 486	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
131	129, 130	eqbrtrd 5170	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑)
132		elbl3 23890	. . . . . . . . . . . . . . . . 17 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ↔ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑))
133	132	biimpar 479	. . . . . . . . . . . . . . . 16 ⊢ (((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) ∧ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
134	123, 126, 131, 133	syl21anc 837	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
135	119, 134	syldan 592	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
136	135	ex 414	. . . . . . . . . . . . 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 6843	. . . . . . . . . . . . . . 15 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ))
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)
140		f1ofun 6833	. . . . . . . . . . . . . 14 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → Fun ^◡𝐺)
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun ^◡𝐺
142		f1odm 6835	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → dom ^◡𝐺 = ℂ)
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ^◡𝐺 = ℂ
144	116, 143	eleqtrrdi 2845	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ dom ^◡𝐺)
145		funfvima 7229	. . . . . . . . . . . . 13 ⊢ ((Fun ^◡𝐺 ∧ (𝐺‘𝑥) ∈ dom ^◡𝐺) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
146	141, 144, 145	sylancr 588	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
147	107, 110	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
148		f1ocnvfv1 7271	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
149	147, 100, 148	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
150	149	eleq1d 2819	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ↔ 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
151	150	biimpd 228	. . . . . . . . . . . 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 408	. . . . . . . . . 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 414	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
156	155	ssrdv 3988	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
157	156	ralrimiva 3147	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
158	103	mpofun 7529	. . . . . . . . . 10 ⊢ Fun 𝐺
159	158	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺)
160	13	sselda 3982	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ × ℝ))
161		f1odm 6835	. . . . . . . . . . 11 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → dom 𝐺 = (ℝ × ℝ))
162	107, 110, 161	mp2b 10	. . . . . . . . . 10 ⊢ dom 𝐺 = (ℝ × ℝ)
163	160, 162	eleqtrrdi 2845	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺)
164		simpr 486	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
165		funfvima 7229	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ 𝐴 → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴)))
166	165	imp 408	. . . . . . . . 9 ⊢ (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
167	159, 163, 164, 166	syl21anc 837	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
168		hmeoima 23261	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) ∧ 𝐴 ∈ (𝐽 ×_t 𝐽)) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
169	107, 168	mpan 689	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
170	106	cnfldtopn 24290	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
171	170	elmopn2 23943	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∈ (∞Met‘ℂ) → ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))))
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
173	172	simprbi 498	. . . . . . . . . 10 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
174	169, 173	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
175	174	adantr 482	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
176		oveq1 7413	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑋) → (𝑚(ball‘(abs ∘ − ))𝑑) = ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
177	176	sseq1d 4013	. . . . . . . . . 10 ⊢ (𝑚 = (𝐺‘𝑋) → ((𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
178	177	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑚 = (𝐺‘𝑋) → (∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
179	178	rspcva 3611	. . . . . . . 8 ⊢ (((𝐺‘𝑋) ∈ (𝐺 “ 𝐴) ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
180	167, 175, 179	syl2anc 585	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
181		imass2 6099	. . . . . . . . . 10 ⊢ (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)))
182		f1of1 6830	. . . . . . . . . . . . 13 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–1-1→ℂ)
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12 ⊢ 𝐺:(ℝ × ℝ)–1-1→ℂ
184		f1imacnv 6847	. . . . . . . . . . . 12 ⊢ ((𝐺:(ℝ × ℝ)–1-1→ℂ ∧ 𝐴 ⊆ (ℝ × ℝ)) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
185	183, 13, 184	sylancr 588	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
186	185	sseq2d 4014	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ((^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)) ↔ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
187	181, 186	imbitrid 243	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
188	187	reximdv 3171	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
189	188	adantr 482	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
190	180, 189	mpd 15	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴)
191		r19.29 3115	. . . . . 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 585	. . . . 5 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ∧ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
193		sstr 3990	. . . . . 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 3085	. . . . 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 3115	. . . 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 585	. . 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 3115	. . 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 585	. 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 2823	. . . . 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 4007	. . . . 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 632	. . . 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 3613	. . 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 3152	. 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 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ⊆ wss 3948 𝒫 cpw 4602 ∪ cuni 4908 class class class wbr 5148 × cxp 5674 ^◡ccnv 5675 dom cdm 5676 ran crn 5677 “ cima 5679 ∘ ccom 5680 Fun wfun 6535 Fn wfn 6536 ⟶wf 6537 –1-1→wf1 6538 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7406 ∈ cmpo 7408 1^st c1st 7970 2^nd c2nd 7971 ℂcc 11105 ℝcr 11106 ici 11109 + caddc 11110 · cmul 11112 +∞cpnf 11242 -∞cmnf 11243 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 − cmin 11441 / cdiv 11868 2c2 12264 ℝ⁺crp 12971 (,)cioo 13321 ℜcre 15041 ℑcim 15042 abscabs 15178 TopOpenctopn 17364 topGenctg 17380 ∞Metcxmet 20922 ballcbl 20924 ℂ_fldccnfld 20937 Topctop 22387 ×_t ctx 23056 Homeochmeo 23249

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ioo 13325 df-icc 13328 df-fz 13482 df-fzo 13625 df-seq 13964 df-exp 14025 df-hash 14288 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cn 22723 df-cnp 22724 df-tx 23058 df-hmeo 23251 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386

This theorem is referenced by: dya2iocnei 33270

W3C validator