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 31148

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 12734	. . . . . . . . . 10 ⊢ (,) = (𝑥 ∈ ℝ^, 𝑦 ∈ ℝ^ ↦ {𝑧 ∈ ℝ^* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)})
2	1	ixxf 12740	. . . . . . . . 9 ⊢ (,):(ℝ^* × ℝ^)⟶𝒫 ℝ^
3		ffn 6507	. . . . . . . . 9 ⊢ ((,):(ℝ^* × ℝ^)⟶𝒫 ℝ^ → (,) Fn (ℝ^* × ℝ^*))
4	2, 3	mp1i 13	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (,) Fn (ℝ^* × ℝ^*))
5		elssuni 4859	. . . . . . . . . . . . . 14 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ ∪ (𝐽 ×_t 𝐽))
6		tpr2rico.0	. . . . . . . . . . . . . . . 16 ⊢ 𝐽 = (topGen‘ran (,))
7		retop 23362	. . . . . . . . . . . . . . . 16 ⊢ (topGen‘ran (,)) ∈ Top
8	6, 7	eqeltri 2907	. . . . . . . . . . . . . . 15 ⊢ 𝐽 ∈ Top
9		uniretop 23363	. . . . . . . . . . . . . . . 16 ⊢ ℝ = ∪ (topGen‘ran (,))
10	6	unieqi 4839	. . . . . . . . . . . . . . . 16 ⊢ ∪ 𝐽 = ∪ (topGen‘ran (,))
11	9, 10	eqtr4i 2845	. . . . . . . . . . . . . . 15 ⊢ ℝ = ∪ 𝐽
12	8, 8, 11, 11	txunii 22193	. . . . . . . . . . . . . 14 ⊢ (ℝ × ℝ) = ∪ (𝐽 ×_t 𝐽)
13	5, 12	sseqtrrdi 4016	. . . . . . . . . . . . 13 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → 𝐴 ⊆ (ℝ × ℝ))
14	13	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐴 ⊆ (ℝ × ℝ))
15		simplr 767	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ 𝐴)
16	14, 15	sseldd 3966	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (ℝ × ℝ))
17		xp1st 7713	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (1^st ‘𝑋) ∈ ℝ)
18	16, 17	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ)
19		simpr 487	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ⁺)
20	19	rpred 12423	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑑 ∈ ℝ)
21	20	rehalfcld 11876	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ)
22	18, 21	resubcld 11060	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
23	22	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
24	18, 21	readdcld 10662	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
25	24	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
26		fnovrn 7315	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
27	4, 23, 25, 26	syl3anc 1366	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
28		xp2nd 7714	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (ℝ × ℝ) → (2^nd ‘𝑋) ∈ ℝ)
29	16, 28	syl 17	. . . . . . . . . 10 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ)
30	29, 21	resubcld 11060	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ)
31	30	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^*)
32	29, 21	readdcld 10662	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ)
33	32	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*)
34		fnovrn 7315	. . . . . . . 8 ⊢ (((,) Fn (ℝ^* × ℝ^) ∧ ((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^ ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^*) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
35	4, 31, 33, 34	syl3anc 1366	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ∈ ran (,))
36		eqidd 2820	. . . . . . 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 5562	. . . . . . . . 9 ⊢ (𝑥 = (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) → (𝑥 × 𝑦) = ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × 𝑦))
38	37	eqeq2d 2830	. . . . . . . 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 5569	. . . . . . . . 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 2830	. . . . . . . 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 3633	. . . . . . 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 1366	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ∃𝑥 ∈ ran (,)∃𝑦 ∈ ran (,)((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) = (𝑥 × 𝑦))
43		eqid 2819	. . . . . . 7 ⊢ (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) = (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
44		vex 3496	. . . . . . . 8 ⊢ 𝑥 ∈ V
45		vex 3496	. . . . . . . 8 ⊢ 𝑦 ∈ V
46	44, 45	xpex 7468	. . . . . . 7 ⊢ (𝑥 × 𝑦) ∈ V
47	43, 46	elrnmpo 7279	. . . . . 6 ⊢ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)) ↔ ∃𝑥 ∈ ran (,)∃𝑦 ∈ ran (,)((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) = (𝑥 × 𝑦))
48	42, 47	sylibr 236	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦)))
49		tpr2rico.2	. . . . 5 ⊢ 𝐵 = ran (𝑥 ∈ ran (,), 𝑦 ∈ ran (,) ↦ (𝑥 × 𝑦))
50	48, 49	eleqtrrdi 2922	. . . 4 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
51	50	ralrimiva 3180	. . 3 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵)
52		xpss 5564	. . . . . . 7 ⊢ (ℝ × ℝ) ⊆ (V × V)
53	52, 16	sseldi 3963	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ (V × V))
54	18	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ ℝ^*)
55	19	rphalfcld 12435	. . . . . . . . 9 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑑 / 2) ∈ ℝ⁺)
56	18, 55	ltsubrpd 12455	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) − (𝑑 / 2)) < (1^st ‘𝑋))
57	18, 55	ltaddrpd 12456	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) < ((1^st ‘𝑋) + (𝑑 / 2)))
58		elioo1 12770	. . . . . . . . 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 586	. . . . . . . 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 1337	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))))
61	29	rexrd 10683	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ ℝ^*)
62	29, 55	ltsubrpd 12455	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) − (𝑑 / 2)) < (2^nd ‘𝑋))
63	29, 55	ltaddrpd 12456	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) < ((2^nd ‘𝑋) + (𝑑 / 2)))
64		elioo1 12770	. . . . . . . . 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 586	. . . . . . . 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 1337	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))
67	60, 66	jca 514	. . . . . 6 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) ∈ (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ∧ (2^nd ‘𝑋) ∈ (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
68		elxp7 7716	. . . . . 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 585	. . . . 5 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
70	69	ralrimiva 3180	. . . 4 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ 𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))))
71		mnfle 12521	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
72	23, 71	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)))
73		pnfge 12517	. . . . . . . . . . . . . . . . . 18 ⊢ (((1^st ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
74	25, 73	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)
75		mnfxr 10690	. . . . . . . . . . . . . . . . . 18 ⊢ -∞ ∈ ℝ^*
76		pnfxr 10687	. . . . . . . . . . . . . . . . . 18 ⊢ +∞ ∈ ℝ^*
77		ioossioo 12821	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
78	75, 76, 77	mpanl12 700	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((1^st ‘𝑋) − (𝑑 / 2)) ∧ ((1^st ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
79	72, 74, 78	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
80		ioomax 12803	. . . . . . . . . . . . . . . 16 ⊢ (-∞(,)+∞) = ℝ
81	79, 80	sseqtrdi 4015	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
82		mnfle 12521	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) − (𝑑 / 2)) ∈ ℝ^* → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
83	31, 82	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → -∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)))
84		pnfge 12517	. . . . . . . . . . . . . . . . . 18 ⊢ (((2^nd ‘𝑋) + (𝑑 / 2)) ∈ ℝ^* → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
85	33, 84	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)
86		ioossioo 12821	. . . . . . . . . . . . . . . . . 18 ⊢ (((-∞ ∈ ℝ^* ∧ +∞ ∈ ℝ^*) ∧ (-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞)) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
87	75, 76, 86	mpanl12 700	. . . . . . . . . . . . . . . . 17 ⊢ ((-∞ ≤ ((2^nd ‘𝑋) − (𝑑 / 2)) ∧ ((2^nd ‘𝑋) + (𝑑 / 2)) ≤ +∞) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
88	83, 85, 87	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ (-∞(,)+∞))
89	88, 80	sseqtrdi 4015	. . . . . . . . . . . . . . 15 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))) ⊆ ℝ)
90		xpss12 5563	. . . . . . . . . . . . . . 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 586	. . . . . . . . . . . . . 14 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (ℝ × ℝ))
92	91	sselda 3965	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2))))) → 𝑥 ∈ (ℝ × ℝ))
93	92	expcom 416	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝑥 ∈ (ℝ × ℝ)))
94	93	ancld 553	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ))))
95	94	imdistanri 572	. . . . . . . . . 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 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝐴 ⊆ (ℝ × ℝ))
97		simpr1 1189	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ 𝐴)
98	96, 97	sseldd 3966	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ⁺ ∧ 𝑥 ∈ (ℝ × ℝ))) → 𝑋 ∈ (ℝ × ℝ))
99	98	3anassrs 1355	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑋 ∈ (ℝ × ℝ))
100		simpr 487	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑥 ∈ (ℝ × ℝ))
101		simplr 767	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ⁺)
102	101	rphalfcld 12435	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑑 / 2) ∈ ℝ⁺)
103		tpr2rico.1	. . . . . . . . . . . . . . 15 ⊢ 𝐺 = (𝑢 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑢 + (i · 𝑣)))
104	103	cnre2csqima 31147	. . . . . . . . . . . . . 14 ⊢ ((𝑋 ∈ (ℝ × ℝ) ∧ 𝑥 ∈ (ℝ × ℝ) ∧ (𝑑 / 2) ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
105	99, 100, 102, 104	syl3anc 1366	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))))
106		eqid 2819	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
107	103, 6, 106	cnrehmeo 23549	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld))
108	106	cnfldtopon 23383	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
109	108	toponunii 21516	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
110	12, 109	hmeof1o 22364	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
111		f1of 6608	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)⟶ℂ)
112	107, 110, 111	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝐺:(ℝ × ℝ)⟶ℂ
113	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)⟶ℂ)
114	113, 99	ffvelrnd 6845	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑋) ∈ ℂ)
115	112	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → 𝐺:(ℝ × ℝ)⟶ℂ)
116	115	ffvelrnda 6844	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ ℂ)
117		sqsscirc2 31145	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ) ∧ 𝑑 ∈ ℝ⁺) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
118	114, 116, 101, 117	syl21anc 835	. . . . . . . . . . . . . . . 16 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2)) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑))
119	118	imp 409	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
120	101	rpxrd 12424	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝑑 ∈ ℝ^*)
121	120	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → 𝑑 ∈ ℝ^*)
122		cnxmet 23373	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
123	121, 122	jctil 522	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*))
124	114	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑋) ∈ ℂ)
125	116	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ℂ)
126	124, 125	jca 514	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ))
127		eqid 2819	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs ∘ − ) = (abs ∘ − )
128	127	cnmetdval 23371	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐺‘𝑥) ∈ ℂ ∧ (𝐺‘𝑋) ∈ ℂ) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
129	125, 124, 128	syl2anc 586	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) = (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))))
130		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑)
131	129, 130	eqbrtrd 5079	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑)
132		elbl3 22994	. . . . . . . . . . . . . . . . 17 ⊢ ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ↔ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑))
133	132	biimpar 480	. . . . . . . . . . . . . . . 16 ⊢ (((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑑 ∈ ℝ^*) ∧ ((𝐺‘𝑋) ∈ ℂ ∧ (𝐺‘𝑥) ∈ ℂ)) ∧ ((𝐺‘𝑥)(abs ∘ − )(𝐺‘𝑋)) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
134	123, 126, 131, 133	syl21anc 835	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ (abs‘((𝐺‘𝑥) − (𝐺‘𝑋))) < 𝑑) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
135	119, 134	syldan 593	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) ∧ ((abs‘(ℜ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2) ∧ (abs‘(ℑ‘((𝐺‘𝑥) − (𝐺‘𝑋)))) < (𝑑 / 2))) → (𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
136	135	ex 415	. . . . . . . . . . . . 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 6620	. . . . . . . . . . . . . . 15 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ))
139	107, 110, 138	mp2b 10	. . . . . . . . . . . . . 14 ⊢ ^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ)
140		f1ofun 6610	. . . . . . . . . . . . . 14 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → Fun ^◡𝐺)
141	139, 140	ax-mp 5	. . . . . . . . . . . . 13 ⊢ Fun ^◡𝐺
142		f1odm 6612	. . . . . . . . . . . . . . 15 ⊢ (^◡𝐺:ℂ–1-1-onto→(ℝ × ℝ) → dom ^◡𝐺 = ℂ)
143	139, 142	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ dom ^◡𝐺 = ℂ
144	116, 143	eleqtrrdi 2922	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝐺‘𝑥) ∈ dom ^◡𝐺)
145		funfvima 6984	. . . . . . . . . . . . 13 ⊢ ((Fun ^◡𝐺 ∧ (𝐺‘𝑥) ∈ dom ^◡𝐺) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
146	141, 144, 145	sylancr 589	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((𝐺‘𝑥) ∈ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) → (^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
147	107, 110	mp1i 13	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → 𝐺:(ℝ × ℝ)–1-1-onto→ℂ)
148		f1ocnvfv1 7025	. . . . . . . . . . . . . . 15 ⊢ ((𝐺:(ℝ × ℝ)–1-1-onto→ℂ ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
149	147, 100, 148	syl2anc 586	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (^◡𝐺‘(𝐺‘𝑥)) = 𝑥)
150	149	eleq1d 2895	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ↔ 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
151	150	biimpd 231	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → ((^◡𝐺‘(𝐺‘𝑥)) ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
152	137, 146, 151	3syld 60	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) ∧ 𝑥 ∈ (ℝ × ℝ)) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
153	152	imp 409	. . . . . . . . . 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 415	. . . . . . . 8 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → (𝑥 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) → 𝑥 ∈ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))))
156	155	ssrdv 3971	. . . . . . 7 ⊢ (((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ⁺) → ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
157	156	ralrimiva 3180	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑑 ∈ ℝ⁺ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)))
158	103	mpofun 7268	. . . . . . . . . 10 ⊢ Fun 𝐺
159	158	a1i 11	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺)
160	13	sselda 3965	. . . . . . . . . 10 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ × ℝ))
161		f1odm 6612	. . . . . . . . . . 11 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → dom 𝐺 = (ℝ × ℝ))
162	107, 110, 161	mp2b 10	. . . . . . . . . 10 ⊢ dom 𝐺 = (ℝ × ℝ)
163	160, 162	eleqtrrdi 2922	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺)
164		simpr 487	. . . . . . . . 9 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴)
165		funfvima 6984	. . . . . . . . . 10 ⊢ ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ 𝐴 → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴)))
166	165	imp 409	. . . . . . . . 9 ⊢ (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
167	159, 163, 164, 166	syl21anc 835	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) ∈ (𝐺 “ 𝐴))
168		hmeoima 22365	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ ((𝐽 ×_t 𝐽)Homeo(TopOpen‘ℂ_fld)) ∧ 𝐴 ∈ (𝐽 ×_t 𝐽)) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
169	107, 168	mpan 688	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld))
170	106	cnfldtopn 23382	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
171	170	elmopn2 23047	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ∈ (∞Met‘ℂ) → ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))))
172	122, 171	ax-mp 5	. . . . . . . . . . 11 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) ↔ ((𝐺 “ 𝐴) ⊆ ℂ ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
173	172	simprbi 499	. . . . . . . . . 10 ⊢ ((𝐺 “ 𝐴) ∈ (TopOpen‘ℂ_fld) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
174	169, 173	syl 17	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
175	174	adantr 483	. . . . . . . 8 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
176		oveq1 7155	. . . . . . . . . . 11 ⊢ (𝑚 = (𝐺‘𝑋) → (𝑚(ball‘(abs ∘ − ))𝑑) = ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑))
177	176	sseq1d 3996	. . . . . . . . . 10 ⊢ (𝑚 = (𝐺‘𝑋) → ((𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
178	177	rexbidv 3295	. . . . . . . . 9 ⊢ (𝑚 = (𝐺‘𝑋) → (∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) ↔ ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)))
179	178	rspcva 3619	. . . . . . . 8 ⊢ (((𝐺‘𝑋) ∈ (𝐺 “ 𝐴) ∧ ∀𝑚 ∈ (𝐺 “ 𝐴)∃𝑑 ∈ ℝ⁺ (𝑚(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴)) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
180	167, 175, 179	syl2anc 586	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴))
181		imass2 5958	. . . . . . . . . 10 ⊢ (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)))
182		f1of1 6607	. . . . . . . . . . . . 13 ⊢ (𝐺:(ℝ × ℝ)–1-1-onto→ℂ → 𝐺:(ℝ × ℝ)–1-1→ℂ)
183	107, 110, 182	mp2b 10	. . . . . . . . . . . 12 ⊢ 𝐺:(ℝ × ℝ)–1-1→ℂ
184		f1imacnv 6624	. . . . . . . . . . . 12 ⊢ ((𝐺:(ℝ × ℝ)–1-1→ℂ ∧ 𝐴 ⊆ (ℝ × ℝ)) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
185	183, 13, 184	sylancr 589	. . . . . . . . . . 11 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (^◡𝐺 “ (𝐺 “ 𝐴)) = 𝐴)
186	185	sseq2d 3997	. . . . . . . . . 10 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → ((^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ (^◡𝐺 “ (𝐺 “ 𝐴)) ↔ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
187	181, 186	syl5ib 246	. . . . . . . . 9 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
188	187	reximdv 3271	. . . . . . . 8 ⊢ (𝐴 ∈ (𝐽 ×_t 𝐽) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
189	188	adantr 483	. . . . . . 7 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → (∃𝑑 ∈ ℝ⁺ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑) ⊆ (𝐺 “ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
190	180, 189	mpd 15	. . . . . 6 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴)
191		r19.29 3252	. . . . . 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 586	. . . . 5 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑑 ∈ ℝ⁺ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ∧ (^◡𝐺 “ ((𝐺‘𝑋)(ball‘(abs ∘ − ))𝑑)) ⊆ 𝐴))
193		sstr 3973	. . . . . 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 3241	. . . . 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 3252	. . . 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 586	. . 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 3252	. . 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 586	. 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 2899	. . . . 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 3990	. . . . 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 3621	. . 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 3280	. 2 ⊢ (∃𝑑 ∈ ℝ⁺ (((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∈ 𝐵 ∧ (𝑋 ∈ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ∧ ((((1^st ‘𝑋) − (𝑑 / 2))(,)((1^st ‘𝑋) + (𝑑 / 2))) × (((2^nd ‘𝑋) − (𝑑 / 2))(,)((2^nd ‘𝑋) + (𝑑 / 2)))) ⊆ 𝐴)) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))
205	199, 204	syl 17	1 ⊢ ((𝐴 ∈ (𝐽 ×_t 𝐽) ∧ 𝑋 ∈ 𝐴) → ∃𝑟 ∈ 𝐵 (𝑋 ∈ 𝑟 ∧ 𝑟 ⊆ 𝐴))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1082 = wceq 1531 ∈ wcel 2108 ∀wral 3136 ∃wrex 3137 Vcvv 3493 ⊆ wss 3934 𝒫 cpw 4537 ∪ cuni 4830 class class class wbr 5057 × cxp 5546 ^◡ccnv 5547 dom cdm 5548 ran crn 5549 “ cima 5551 ∘ ccom 5552 Fun wfun 6342 Fn wfn 6343 ⟶wf 6344 –1-1→wf1 6345 –1-1-onto→wf1o 6347 ‘cfv 6348 (class class class)co 7148 ∈ cmpo 7150 1^st c1st 7679 2^nd c2nd 7680 ℂcc 10527 ℝcr 10528 ici 10531 + caddc 10532 · cmul 10534 +∞cpnf 10664 -∞cmnf 10665 ℝ^*cxr 10666 < clt 10667 ≤ cle 10668 − cmin 10862 / cdiv 11289 2c2 11684 ℝ⁺crp 12381 (,)cioo 12730 ℜcre 14448 ℑcim 14449 abscabs 14585 TopOpenctopn 16687 topGenctg 16703 ∞Metcxmet 20522 ballcbl 20524 ℂ_fldccnfld 20537 Topctop 21493 ×_t ctx 22160 Homeochmeo 22353

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-rep 5181 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 ax-cnex 10585 ax-resscn 10586 ax-1cn 10587 ax-icn 10588 ax-addcl 10589 ax-addrcl 10590 ax-mulcl 10591 ax-mulrcl 10592 ax-mulcom 10593 ax-addass 10594 ax-mulass 10595 ax-distr 10596 ax-i2m1 10597 ax-1ne0 10598 ax-1rid 10599 ax-rnegex 10600 ax-rrecex 10601 ax-cnre 10602 ax-pre-lttri 10603 ax-pre-lttrn 10604 ax-pre-ltadd 10605 ax-pre-mulgt0 10606 ax-pre-sup 10607 ax-addf 10608 ax-mulf 10609

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-nel 3122 df-ral 3141 df-rex 3142 df-reu 3143 df-rmo 3144 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-pss 3952 df-nul 4290 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-uni 4831 df-int 4868 df-iun 4912 df-iin 4913 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-se 5508 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-isom 6357 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-of 7401 df-om 7573 df-1st 7681 df-2nd 7682 df-supp 7823 df-wrecs 7939 df-recs 8000 df-rdg 8038 df-1o 8094 df-2o 8095 df-oadd 8098 df-er 8281 df-map 8400 df-ixp 8454 df-en 8502 df-dom 8503 df-sdom 8504 df-fin 8505 df-fsupp 8826 df-fi 8867 df-sup 8898 df-inf 8899 df-oi 8966 df-card 9360 df-pnf 10669 df-mnf 10670 df-xr 10671 df-ltxr 10672 df-le 10673 df-sub 10864 df-neg 10865 df-div 11290 df-nn 11631 df-2 11692 df-3 11693 df-4 11694 df-5 11695 df-6 11696 df-7 11697 df-8 11698 df-9 11699 df-n0 11890 df-z 11974 df-dec 12091 df-uz 12236 df-q 12341 df-rp 12382 df-xneg 12499 df-xadd 12500 df-xmul 12501 df-ioo 12734 df-icc 12737 df-fz 12885 df-fzo 13026 df-seq 13362 df-exp 13422 df-hash 13683 df-cj 14450 df-re 14451 df-im 14452 df-sqrt 14586 df-abs 14587 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-starv 16572 df-sca 16573 df-vsca 16574 df-ip 16575 df-tset 16576 df-ple 16577 df-ds 16579 df-unif 16580 df-hom 16581 df-cco 16582 df-rest 16688 df-topn 16689 df-0g 16707 df-gsum 16708 df-topgen 16709 df-pt 16710 df-prds 16713 df-xrs 16767 df-qtop 16772 df-imas 16773 df-xps 16775 df-mre 16849 df-mrc 16850 df-acs 16852 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-mulg 18217 df-cntz 18439 df-cmn 18900 df-psmet 20529 df-xmet 20530 df-met 20531 df-bl 20532 df-mopn 20533 df-cnfld 20538 df-top 21494 df-topon 21511 df-topsp 21533 df-bases 21546 df-cn 21827 df-cnp 21828 df-tx 22162 df-hmeo 22355 df-xms 22922 df-ms 22923 df-tms 22924 df-cncf 23478

This theorem is referenced by: dya2iocnei 31533

W3C validator