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 33898

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 13271	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxf 13277	. . . . . . . . 9 ⊢ (,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
3		ffn 6656	. . . . . . . . 9 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ^ → (,) Fn (ℝ^* × ℝ^*))
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (,) Fn (ℝ^* × ℝ^*))
5		elssuni 4891	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ ∪ (𝐽 ×_t 𝐽))
6		tpr2rico.0	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (topGen‘ran (,))
7		retop 24666	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) ∈ Top
8	6, 7	eqeltri 2824	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
9		uniretop 24667	. . . . . . . . . . . . . . . 16 ⊢ ℝ = ∪ (topGen‘ran (,))
10	6	unieqi 4873	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
11	9, 10	eqtr4i 2755	. . . . . . . . . . . . . . 15 ⊢ ℝ = ∪ 𝐽
12	8, 8, 11, 11	txunii 23497	. . . . . . . . . . . . . 14 ⊢ (ℝ × ℝ) = ∪ (𝐽 ×_t 𝐽)
13	5, 12	sseqtrrdi 3979	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ (ℝ × ℝ))
14	13	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐴 ⊆ (ℝ × ℝ))
15		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ 𝐴)
16	14, 15	sseldd 3938	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (ℝ × ℝ))
17		xp1st 7963	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (1^st ‘𝑋) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ)
19		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ⁺)
20	19	rpred 12956	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ)
21	20	rehalfcld 12390	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ)
22	18, 21	resubcld 11567	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
23	22	rexrd 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
24	18, 21	readdcld 11163	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
25	24	rexrd 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
26		fnovrn 7528	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
27	4, 23, 25, 26	syl3anc 1373	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
28		xp2nd 7964	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (2^nd ‘𝑋) ∈ ℝ)
29	16, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ)
30	29, 21	resubcld 11567	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
31	30	rexrd 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
32	29, 21	readdcld 11163	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
33	32	rexrd 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
34		fnovrn 7528	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
35	4, 31, 33, 34	syl3anc 1373	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
36		eqidd 2730	. . . . . . 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 5637	. . . . . . . . 9 ⊢ (𝑥 = (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) → (𝑥 × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦))
38	37	eqeq2d 2740	. . . . . . . 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 5644	. . . . . . . . 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 2740	. . . . . . . 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 3592	. . . . . . 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 1373	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ∃𝑥 ∈ ran (,)∃𝑦 ∈ ran (,)((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) = (𝑥 × 𝑦))
43		eqid 2729	. . . . . . 7 ⊢ (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) = (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
44		vex 3442	. . . . . . . 8 ⊢ 𝑥 ∈ V
45		vex 3442	. . . . . . . 8 ⊢ 𝑦 ∈ V
46	44, 45	xpex 7693	. . . . . . 7 ⊢ (𝑥 × 𝑦) ∈ V
47	43, 46	elrnmpo 7489	. . . . . 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 234	. . . . 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 2839	. . . 4 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
51	50	ralrimiva 3121	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
52		xpss 5639	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (V × V)
53	52, 16	sselid 3935	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (V × V))
54	18	rexrd 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ^*)
55	19	rphalfcld 12968	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ⁺)
56	18, 55	ltsubrpd 12988	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋))
57	18, 55	ltaddrpd 12989	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))
58		elioo1 13307	. . . . . . . . 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 584	. . . . . . . 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 11184	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ^*)
62	29, 55	ltsubrpd 12988	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋))
63	29, 55	ltaddrpd 12989	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))
64		elioo1 13307	. . . . . . . . 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 584	. . . . . . . 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 511	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∧ (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
68		elxp7 7966	. . . . . 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 583	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
70	69	ralrimiva 3121	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
71		mnfle 13056	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
73		pnfge 13051	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
75		mnfxr 11191	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
76		pnfxr 11188	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
77		ioossioo 13363	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
78	75, 76, 77	mpanl12 702	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
79	72, 74, 78	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
80		ioomax 13344	. . . . . . . . . . . . . . . 16 ⊢ (-∞(,)+∞) = ℝ
81	79, 80	sseqtrdi 3978	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
82		mnfle 13056	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
84		pnfge 13051	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
86		ioossioo 13363	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
87	75, 76, 86	mpanl12 702	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
88	83, 85, 87	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
89	88, 80	sseqtrdi 3978	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
90		xpss12 5638	. . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (ℝ × ℝ))
92	91	sselda 3937	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (ℝ × ℝ))
93	92	expcom 413	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑥 ∈ (ℝ × ℝ)))
94	93	ancld 550	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ))))
95	94	imdistanri 569	. . . . . . . . . 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 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝐴 ⊆ (ℝ × ℝ))
97		simpr1 1195	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ 𝐴)
98	96, 97	sseldd 3938	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ (ℝ × ℝ))
99	98	3anassrs 1361	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑋 ∈ (ℝ × ℝ))
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑥 ∈ (ℝ × ℝ))
101		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ⁺)
102	101	rphalfcld 12968	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑑 / 2) ∈ ℝ⁺)
103		tpr2rico.1	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
104	103	cnre2csqima 33897	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑥 ∈ (ℝ × ℝ) ∧ (𝑑 / 2) ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
105	99, 100, 102, 104	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
106		eqid 2729	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
107	103, 6, 106	cnrehmeo 24868	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld))
108	106	cnfldtopon 24687	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
109	108	toponunii 22820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
110	12, 109	hmeof1o 23668	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
111		f1of 6768	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)⟶ℂ)
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺:(ℝ × ℝ)⟶ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)⟶ℂ)
114	113, 99	ffvelcdmd 7023	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑋) ∈ ℂ)
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐺:(ℝ × ℝ)⟶ℂ)
116	115	ffvelcdmda 7022	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ ℂ)
117		sqsscirc2 33895	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) ∧ 𝑑 ∈ ℝ⁺) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
118	114, 116, 101, 117	syl21anc 837	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
119	118	imp 406	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
120	101	rpxrd 12957	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ^*)
121	120	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → 𝑑 ∈ ℝ^*)
122		cnxmet 24677	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
123	121, 122	jctil 519	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*))
124	114	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑋) ∈ ℂ)
125	116	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ℂ)
126	124, 125	jca 511	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ))
127		eqid 2729	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
128	127	cnmetdval 24675	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑋) ∈ ℂ) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
129	125, 124, 128	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
130		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
131	129, 130	eqbrtrd 5117	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑)
132		elbl3 24297	. . . . . . . . . . . . . . . . 17 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ↔ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑))
133	132	biimpar 477	. . . . . . . . . . . . . . . 16 ⊢ (((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) ∧ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
134	123, 126, 131, 133	syl21anc 837	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
135	119, 134	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
136	135	ex 412	. . . . . . . . . . . . 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 6780	. . . . . . . . . . . . . . 15 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ))
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)
140		f1ofun 6770	. . . . . . . . . . . . . 14 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → Fun ^◡𝐺)
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun ^◡𝐺
142		f1odm 6772	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → dom ^◡𝐺 = ℂ)
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ^◡𝐺 = ℂ
144	116, 143	eleqtrrdi 2839	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ dom ^◡𝐺)
145		funfvima 7170	. . . . . . . . . . . . 13 ⊢ ((Fun ^◡𝐺 ∧ (𝐺‘𝑥) ∈ dom ^◡𝐺) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
146	141, 144, 145	sylancr 587	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
147	107, 110	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
148		f1ocnvfv1 7217	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
149	147, 100, 148	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
150	149	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ↔ 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
151	150	biimpd 229	. . . . . . . . . . . 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 406	. . . . . . . . . 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 412	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
156	155	ssrdv 3943	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
157	156	ralrimiva 3121	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
158	103	mpofun 7477	. . . . . . . . . 10 ⊢ Fun 𝐺
159	158	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺)
160	13	sselda 3937	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ × ℝ))
161		f1odm 6772	. . . . . . . . . . 11 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → dom 𝐺 = (ℝ × ℝ))
162	107, 110, 161	mp2b 10	. . . . . . . . . 10 ⊢ dom 𝐺 = (ℝ × ℝ)
163	160, 162	eleqtrrdi 2839	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺)
164		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
165		funfvima 7170	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ 𝐴 → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴)))
166	165	imp 406	. . . . . . . . 9 ⊢ (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
167	159, 163, 164, 166	syl21anc 837	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
168		hmeoima 23669	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) ∧ 𝐴 ∈ (𝐽 ×_t 𝐽)) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
169	107, 168	mpan 690	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
170	106	cnfldtopn 24686	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
171	170	elmopn2 24350	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∈ (∞Met‘ℂ) → ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))))
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
173	172	simprbi 496	. . . . . . . . . 10 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
174	169, 173	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
175	174	adantr 480	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
176		oveq1 7360	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑋) → (𝑚(ball‘(abs ∘ − ))𝑑) = ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
177	176	sseq1d 3969	. . . . . . . . . 10 ⊢ (𝑚 = (𝐺‘𝑋) → ((𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
178	177	rexbidv 3153	. . . . . . . . 9 ⊢ (𝑚 = (𝐺‘𝑋) → (∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
179	178	rspcva 3577	. . . . . . . 8 ⊢ (((𝐺‘𝑋) ∈ (𝐺 “ 𝐴) ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
180	167, 175, 179	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
181		imass2 6057	. . . . . . . . . 10 ⊢ (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)))
182		f1of1 6767	. . . . . . . . . . . . 13 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–1-1→ℂ)
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12 ⊢ 𝐺:(ℝ × ℝ)–1-1→ℂ
184		f1imacnv 6784	. . . . . . . . . . . 12 ⊢ ((𝐺:(ℝ × ℝ)–1-1→ℂ ∧ 𝐴 ⊆ (ℝ × ℝ)) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
185	183, 13, 184	sylancr 587	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
186	185	sseq2d 3970	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ((^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)) ↔ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
187	181, 186	imbitrid 244	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
188	187	reximdv 3144	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
189	188	adantr 480	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
190	180, 189	mpd 15	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴)
191		r19.29 3092	. . . . . 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 584	. . . . 5 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ∧ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
193		sstr 3946	. . . . . 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 3067	. . . . 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 3092	. . . 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 584	. . 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 3092	. . 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 584	. 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 2817	. . . . 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 3963	. . . . 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 3579	. . 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 3126	. 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 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ∀wral 3044 ∃wrex 3053 Vcvv 3438 ⊆ wss 3905 𝒫 cpw 4553 ∪ cuni 4861 class class class wbr 5095 × cxp 5621 ^◡ccnv 5622 dom cdm 5623 ran crn 5624 “ cima 5626 ∘ ccom 5627 Fun wfun 6480 Fn wfn 6481 ⟶wf 6482 –1-1→wf1 6483 –1-1-onto→wf1o 6485 ‘cfv 6486 (class class class)co 7353 ∈ cmpo 7355 1^st c1st 7929 2^nd c2nd 7930 ℂcc 11026 ℝcr 11027 ici 11030 + caddc 11031 · cmul 11033 +∞cpnf 11165 -∞cmnf 11166 ℝ^*cxr 11167 < clt 11168 ≤ cle 11169 − cmin 11366 / cdiv 11796 2c2 12202 ℝ⁺crp 12912 (,)cioo 13267 ℜcre 15023 ℑcim 15024 abscabs 15160 TopOpenctopn 17344 topGenctg 17360 ∞Metcxmet 21265 ballcbl 21267 ℂ_fldccnfld 21280 Topctop 22797 ×_t ctx 23464 Homeochmeo 23657

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105 ax-pre-sup 11106 ax-addf 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-om 7807 df-1st 7931 df-2nd 7932 df-supp 8101 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-2o 8396 df-er 8632 df-map 8762 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-fi 9320 df-sup 9351 df-inf 9352 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11368 df-neg 11369 df-div 11797 df-nn 12148 df-2 12210 df-3 12211 df-4 12212 df-5 12213 df-6 12214 df-7 12215 df-8 12216 df-9 12217 df-n0 12404 df-z 12491 df-dec 12611 df-uz 12755 df-q 12869 df-rp 12913 df-xneg 13033 df-xadd 13034 df-xmul 13035 df-ioo 13271 df-icc 13274 df-fz 13430 df-fzo 13577 df-seq 13928 df-exp 13988 df-hash 14257 df-cj 15025 df-re 15026 df-im 15027 df-sqrt 15161 df-abs 15162 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17140 df-ress 17161 df-plusg 17193 df-mulr 17194 df-starv 17195 df-sca 17196 df-vsca 17197 df-ip 17198 df-tset 17199 df-ple 17200 df-ds 17202 df-unif 17203 df-hom 17204 df-cco 17205 df-rest 17345 df-topn 17346 df-0g 17364 df-gsum 17365 df-topgen 17366 df-pt 17367 df-prds 17370 df-xrs 17425 df-qtop 17430 df-imas 17431 df-xps 17433 df-mre 17507 df-mrc 17508 df-acs 17510 df-mgm 18533 df-sgrp 18612 df-mnd 18628 df-submnd 18677 df-mulg 18966 df-cntz 19215 df-cmn 19680 df-psmet 21272 df-xmet 21273 df-met 21274 df-bl 21275 df-mopn 21276 df-cnfld 21281 df-top 22798 df-topon 22815 df-topsp 22837 df-bases 22850 df-cn 23131 df-cnp 23132 df-tx 23466 df-hmeo 23659 df-xms 24225 df-ms 24226 df-tms 24227 df-cncf 24788

This theorem is referenced by: dya2iocnei 34269

W3C validator