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 33943

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 13366	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxf 13372	. . . . . . . . 9 ⊢ (,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
3		ffn 6706	. . . . . . . . 9 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ^ → (,) Fn (ℝ^* × ℝ^*))
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (,) Fn (ℝ^* × ℝ^*))
5		elssuni 4913	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ ∪ (𝐽 ×_t 𝐽))
6		tpr2rico.0	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (topGen‘ran (,))
7		retop 24700	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) ∈ Top
8	6, 7	eqeltri 2830	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
9		uniretop 24701	. . . . . . . . . . . . . . . 16 ⊢ ℝ = ∪ (topGen‘ran (,))
10	6	unieqi 4895	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
11	9, 10	eqtr4i 2761	. . . . . . . . . . . . . . 15 ⊢ ℝ = ∪ 𝐽
12	8, 8, 11, 11	txunii 23531	. . . . . . . . . . . . . 14 ⊢ (ℝ × ℝ) = ∪ (𝐽 ×_t 𝐽)
13	5, 12	sseqtrrdi 4000	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ (ℝ × ℝ))
14	13	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐴 ⊆ (ℝ × ℝ))
15		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ 𝐴)
16	14, 15	sseldd 3959	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (ℝ × ℝ))
17		xp1st 8020	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (1^st ‘𝑋) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ)
19		simpr 484	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ⁺)
20	19	rpred 13051	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ)
21	20	rehalfcld 12488	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ)
22	18, 21	resubcld 11665	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
23	22	rexrd 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
24	18, 21	readdcld 11264	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
25	24	rexrd 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
26		fnovrn 7582	. . . . . . . 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 8021	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (2^nd ‘𝑋) ∈ ℝ)
29	16, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ)
30	29, 21	resubcld 11665	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
31	30	rexrd 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
32	29, 21	readdcld 11264	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
33	32	rexrd 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
34		fnovrn 7582	. . . . . . . 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 2736	. . . . . . 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 5668	. . . . . . . . 9 ⊢ (𝑥 = (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) → (𝑥 × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦))
38	37	eqeq2d 2746	. . . . . . . 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 5675	. . . . . . . . 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 2746	. . . . . . . 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 3614	. . . . . . 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 2735	. . . . . . 7 ⊢ (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) = (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
44		vex 3463	. . . . . . . 8 ⊢ 𝑥 ∈ V
45		vex 3463	. . . . . . . 8 ⊢ 𝑦 ∈ V
46	44, 45	xpex 7747	. . . . . . 7 ⊢ (𝑥 × 𝑦) ∈ V
47	43, 46	elrnmpo 7543	. . . . . 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 2845	. . . 4 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
51	50	ralrimiva 3132	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
52		xpss 5670	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (V × V)
53	52, 16	sselid 3956	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (V × V))
54	18	rexrd 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ^*)
55	19	rphalfcld 13063	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ⁺)
56	18, 55	ltsubrpd 13083	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋))
57	18, 55	ltaddrpd 13084	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))
58		elioo1 13402	. . . . . . . . 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 11285	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ^*)
62	29, 55	ltsubrpd 13083	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋))
63	29, 55	ltaddrpd 13084	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))
64		elioo1 13402	. . . . . . . . 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 8023	. . . . . 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 3132	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
71		mnfle 13151	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
73		pnfge 13146	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
75		mnfxr 11292	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
76		pnfxr 11289	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
77		ioossioo 13458	. . . . . . . . . . . . . . . . . 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 13439	. . . . . . . . . . . . . . . 16 ⊢ (-∞(,)+∞) = ℝ
81	79, 80	sseqtrdi 3999	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
82		mnfle 13151	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
84		pnfge 13146	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
86		ioossioo 13458	. . . . . . . . . . . . . . . . . 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 3999	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
90		xpss12 5669	. . . . . . . . . . . . . . 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 3958	. . . . . . . . . . . . 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 3959	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ (ℝ × ℝ))
99	98	3anassrs 1361	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑋 ∈ (ℝ × ℝ))
100		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑥 ∈ (ℝ × ℝ))
101		simplr 768	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ⁺)
102	101	rphalfcld 13063	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑑 / 2) ∈ ℝ⁺)
103		tpr2rico.1	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
104	103	cnre2csqima 33942	. . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
107	103, 6, 106	cnrehmeo 24902	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld))
108	106	cnfldtopon 24721	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
109	108	toponunii 22854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
110	12, 109	hmeof1o 23702	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
111		f1of 6818	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)⟶ℂ)
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺:(ℝ × ℝ)⟶ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)⟶ℂ)
114	113, 99	ffvelcdmd 7075	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑋) ∈ ℂ)
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐺:(ℝ × ℝ)⟶ℂ)
116	115	ffvelcdmda 7074	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ ℂ)
117		sqsscirc2 33940	. . . . . . . . . . . . . . . . 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 13052	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ^*)
121	120	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → 𝑑 ∈ ℝ^*)
122		cnxmet 24711	. . . . . . . . . . . . . . . . 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 2735	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
128	127	cnmetdval 24709	. . . . . . . . . . . . . . . . . 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 5141	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑)
132		elbl3 24331	. . . . . . . . . . . . . . . . 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 6830	. . . . . . . . . . . . . . 15 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ))
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)
140		f1ofun 6820	. . . . . . . . . . . . . 14 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → Fun ^◡𝐺)
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun ^◡𝐺
142		f1odm 6822	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → dom ^◡𝐺 = ℂ)
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ^◡𝐺 = ℂ
144	116, 143	eleqtrrdi 2845	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ dom ^◡𝐺)
145		funfvima 7222	. . . . . . . . . . . . 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 7269	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
149	147, 100, 148	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
150	149	eleq1d 2819	. . . . . . . . . . . . 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 3964	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
157	156	ralrimiva 3132	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
158	103	mpofun 7531	. . . . . . . . . 10 ⊢ Fun 𝐺
159	158	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺)
160	13	sselda 3958	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ × ℝ))
161		f1odm 6822	. . . . . . . . . . 11 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → dom 𝐺 = (ℝ × ℝ))
162	107, 110, 161	mp2b 10	. . . . . . . . . 10 ⊢ dom 𝐺 = (ℝ × ℝ)
163	160, 162	eleqtrrdi 2845	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺)
164		simpr 484	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
165		funfvima 7222	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ 𝐴 → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴)))
166	165	imp 406	. . . . . . . . 9 ⊢ (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
167	159, 163, 164, 166	syl21anc 837	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
168		hmeoima 23703	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) ∧ 𝐴 ∈ (𝐽 ×_t 𝐽)) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
169	107, 168	mpan 690	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
170	106	cnfldtopn 24720	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
171	170	elmopn2 24384	. . . . . . . . . . . 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 7412	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑋) → (𝑚(ball‘(abs ∘ − ))𝑑) = ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
177	176	sseq1d 3990	. . . . . . . . . 10 ⊢ (𝑚 = (𝐺‘𝑋) → ((𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
178	177	rexbidv 3164	. . . . . . . . 9 ⊢ (𝑚 = (𝐺‘𝑋) → (∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
179	178	rspcva 3599	. . . . . . . 8 ⊢ (((𝐺‘𝑋) ∈ (𝐺 “ 𝐴) ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
180	167, 175, 179	syl2anc 584	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
181		imass2 6089	. . . . . . . . . 10 ⊢ (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)))
182		f1of1 6817	. . . . . . . . . . . . 13 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–1-1→ℂ)
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12 ⊢ 𝐺:(ℝ × ℝ)–1-1→ℂ
184		f1imacnv 6834	. . . . . . . . . . . 12 ⊢ ((𝐺:(ℝ × ℝ)–1-1→ℂ ∧ 𝐴 ⊆ (ℝ × ℝ)) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
185	183, 13, 184	sylancr 587	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
186	185	sseq2d 3991	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ((^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)) ↔ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
187	181, 186	imbitrid 244	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
188	187	reximdv 3155	. . . . . . . 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 3101	. . . . . 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 3967	. . . . . 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 3074	. . . . 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 3101	. . . 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 3101	. . 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 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 3984	. . . . 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 3601	. . 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 3137	. 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 2108 ∀wral 3051 ∃wrex 3060 Vcvv 3459 ⊆ wss 3926 𝒫 cpw 4575 ∪ cuni 4883 class class class wbr 5119 × cxp 5652 ^◡ccnv 5653 dom cdm 5654 ran crn 5655 “ cima 5657 ∘ ccom 5658 Fun wfun 6525 Fn wfn 6526 ⟶wf 6527 –1-1→wf1 6528 –1-1-onto→wf1o 6530 ‘cfv 6531 (class class class)co 7405 ∈ cmpo 7407 1^st c1st 7986 2^nd c2nd 7987 ℂcc 11127 ℝcr 11128 ici 11131 + caddc 11132 · cmul 11134 +∞cpnf 11266 -∞cmnf 11267 ℝ^*cxr 11268 < clt 11269 ≤ cle 11270 − cmin 11466 / cdiv 11894 2c2 12295 ℝ⁺crp 13008 (,)cioo 13362 ℜcre 15116 ℑcim 15117 abscabs 15253 TopOpenctopn 17435 topGenctg 17451 ∞Metcxmet 21300 ballcbl 21302 ℂ_fldccnfld 21315 Topctop 22831 ×_t ctx 23498 Homeochmeo 23691

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729 ax-cnex 11185 ax-resscn 11186 ax-1cn 11187 ax-icn 11188 ax-addcl 11189 ax-addrcl 11190 ax-mulcl 11191 ax-mulrcl 11192 ax-mulcom 11193 ax-addass 11194 ax-mulass 11195 ax-distr 11196 ax-i2m1 11197 ax-1ne0 11198 ax-1rid 11199 ax-rnegex 11200 ax-rrecex 11201 ax-cnre 11202 ax-pre-lttri 11203 ax-pre-lttrn 11204 ax-pre-ltadd 11205 ax-pre-mulgt0 11206 ax-pre-sup 11207 ax-addf 11208

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 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3359 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-pss 3946 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-tp 4606 df-op 4608 df-uni 4884 df-int 4923 df-iun 4969 df-iin 4970 df-br 5120 df-opab 5182 df-mpt 5202 df-tr 5230 df-id 5548 df-eprel 5553 df-po 5561 df-so 5562 df-fr 5606 df-se 5607 df-we 5608 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-ord 6355 df-on 6356 df-lim 6357 df-suc 6358 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-isom 6540 df-riota 7362 df-ov 7408 df-oprab 7409 df-mpo 7410 df-of 7671 df-om 7862 df-1st 7988 df-2nd 7989 df-supp 8160 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-1o 8480 df-2o 8481 df-er 8719 df-map 8842 df-ixp 8912 df-en 8960 df-dom 8961 df-sdom 8962 df-fin 8963 df-fsupp 9374 df-fi 9423 df-sup 9454 df-inf 9455 df-oi 9524 df-card 9953 df-pnf 11271 df-mnf 11272 df-xr 11273 df-ltxr 11274 df-le 11275 df-sub 11468 df-neg 11469 df-div 11895 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12502 df-z 12589 df-dec 12709 df-uz 12853 df-q 12965 df-rp 13009 df-xneg 13128 df-xadd 13129 df-xmul 13130 df-ioo 13366 df-icc 13369 df-fz 13525 df-fzo 13672 df-seq 14020 df-exp 14080 df-hash 14349 df-cj 15118 df-re 15119 df-im 15120 df-sqrt 15254 df-abs 15255 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17229 df-ress 17252 df-plusg 17284 df-mulr 17285 df-starv 17286 df-sca 17287 df-vsca 17288 df-ip 17289 df-tset 17290 df-ple 17291 df-ds 17293 df-unif 17294 df-hom 17295 df-cco 17296 df-rest 17436 df-topn 17437 df-0g 17455 df-gsum 17456 df-topgen 17457 df-pt 17458 df-prds 17461 df-xrs 17516 df-qtop 17521 df-imas 17522 df-xps 17524 df-mre 17598 df-mrc 17599 df-acs 17601 df-mgm 18618 df-sgrp 18697 df-mnd 18713 df-submnd 18762 df-mulg 19051 df-cntz 19300 df-cmn 19763 df-psmet 21307 df-xmet 21308 df-met 21309 df-bl 21310 df-mopn 21311 df-cnfld 21316 df-top 22832 df-topon 22849 df-topsp 22871 df-bases 22884 df-cn 23165 df-cnp 23166 df-tx 23500 df-hmeo 23693 df-xms 24259 df-ms 24260 df-tms 24261 df-cncf 24822

This theorem is referenced by: dya2iocnei 34314

W3C validator