tpr2rico

Description: For any point of an open set of the usual topology on ( RR X. RR ) 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 ( l ^ +oo ) norm X . (Contributed by Thierry Arnoux, 21-Sep-2017)

	Ref	Expression
Hypotheses	tpr2rico.0	$⊢ J = topGen (ran (.))$
	tpr2rico.1	$⊢ G = (u \in ℝ, v \in ℝ ⟼ u + i v)$
	tpr2rico.2	$⊢ B = ran (x \in ran (.), y \in ran (.) ⟼ x \times y)$
Assertion	tpr2rico	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists r \in B (X \in r \land r \subseteq A)$

Proof

Step	Hyp	Ref	Expression
1		tpr2rico.0	$⊢ J = topGen (ran (.))$
2		tpr2rico.1	$⊢ G = (u \in ℝ, v \in ℝ ⟼ u + i v)$
3		tpr2rico.2	$⊢ B = ran (x \in ran (.), y \in ran (.) ⟼ x \times y)$
4		df-ioo	$⊢ (.) = (x \in ℝ^{}, y \in ℝ^{} ⟼ \{z \in ℝ^{*} \| (x < z \land z < y)\})$
5	4	ixxf	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{*}$
6		ffn	$⊢ (.) : ℝ^{} \times ℝ^{} ⟶ 𝒫 ℝ^{} \to (.) Fn (ℝ^{} \times ℝ^{*})$
7	5 6	mp1i	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (.) Fn (ℝ^{} \times ℝ^{})$
8		elssuni	$⊢ A \in (J \times_{t} J) \to A \subseteq ⋃ (J \times_{t} J)$
9		retop	$⊢ topGen (ran (.)) \in Top$
10	1 9	eqeltri	$⊢ J \in Top$
11		uniretop	$⊢ ℝ = ⋃ topGen (ran (.))$
12	1	unieqi	$⊢ ⋃ J = ⋃ topGen (ran (.))$
13	11 12	eqtr4i	$⊢ ℝ = ⋃ J$
14	10 10 13 13	txunii	$⊢ ℝ^{2} = ⋃ (J \times_{t} J)$
15	8 14	sseqtrrdi	$⊢ A \in (J \times_{t} J) \to A \subseteq ℝ^{2}$
16	15	ad2antrr	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to A \subseteq ℝ^{2}$
17		simplr	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to X \in A$
18	16 17	sseldd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to X \in ℝ^{2}$
19		xp1st	$⊢ X \in ℝ^{2} \to 1^{st} (X) \in ℝ$
20	18 19	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) \in ℝ$
21		simpr	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to d \in ℝ^{+}$
22	21	rpred	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to d \in ℝ$
23	22	rehalfcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to \frac{d}{2} \in ℝ$
24	20 23	resubcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) - (\frac{d}{2}) \in ℝ$
25	24	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) - (\frac{d}{2}) \in ℝ^{*}$
26	20 23	readdcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) + (\frac{d}{2}) \in ℝ$
27	26	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) + (\frac{d}{2}) \in ℝ^{*}$
28		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land 1^{st} (X) - (\frac{d}{2}) \in ℝ^{} \land 1^{st} (X) + (\frac{d}{2}) \in ℝ^{}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \in ran (.)$
29	7 25 27 28	syl3anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \in ran (.)$
30		xp2nd	$⊢ X \in ℝ^{2} \to 2^{nd} (X) \in ℝ$
31	18 30	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) \in ℝ$
32	31 23	resubcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) - (\frac{d}{2}) \in ℝ$
33	32	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) - (\frac{d}{2}) \in ℝ^{*}$
34	31 23	readdcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) + (\frac{d}{2}) \in ℝ$
35	34	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) + (\frac{d}{2}) \in ℝ^{*}$
36		fnovrn	$⊢ ((.) Fn (ℝ^{} \times ℝ^{}) \land 2^{nd} (X) - (\frac{d}{2}) \in ℝ^{} \land 2^{nd} (X) + (\frac{d}{2}) \in ℝ^{}) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in ran (.)$
37	7 33 35 36	syl3anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in ran (.)$
38		eqidd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))$
39		xpeq1	$⊢ x = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \to x \times y = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times y$
40	39	eqeq2d	$⊢ x = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \to ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = x \times y \leftrightarrow (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times y)$
41		xpeq2	$⊢ y = (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times y = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))$
42	41	eqeq2d	$⊢ y = (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \to ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times y \leftrightarrow (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))$
43	40 42	rspc2ev	$⊢ ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \in ran (.) \land (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in ran (.) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to \exists x \in ran (.) \exists y \in ran (.) (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = x \times y$
44	29 37 38 43	syl3anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to \exists x \in ran (.) \exists y \in ran (.) (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = x \times y$
45		eqid	$⊢ (x \in ran (.), y \in ran (.) ⟼ x \times y) = (x \in ran (.), y \in ran (.) ⟼ x \times y)$
46		vex	$⊢ x \in V$
47		vex	$⊢ y \in V$
48	46 47	xpex	$⊢ x \times y \in V$
49	45 48	elrnmpo	$⊢ (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in ran (x \in ran (.), y \in ran (.) ⟼ x \times y) \leftrightarrow \exists x \in ran (.) \exists y \in ran (.) (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) = x \times y$
50	44 49	sylibr	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in ran (x \in ran (.), y \in ran (.) ⟼ x \times y)$
51	50 3	eleqtrrdi	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B$
52	51	ralrimiva	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \forall d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B$
53		xpss	$⊢ ℝ^{2} \subseteq V \times V$
54	53 18	sseldi	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to X \in (V \times V)$
55	20	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) \in ℝ^{*}$
56	21	rphalfcld	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to \frac{d}{2} \in ℝ^{+}$
57	20 56	ltsubrpd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) - (\frac{d}{2}) < 1^{st} (X)$
58	20 56	ltaddrpd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) < 1^{st} (X) + (\frac{d}{2})$
59		elioo1	$⊢ (1^{st} (X) - (\frac{d}{2}) \in ℝ^{} \land 1^{st} (X) + (\frac{d}{2}) \in ℝ^{}) \to (1^{st} (X) \in (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \leftrightarrow (1^{st} (X) \in ℝ^{*} \land 1^{st} (X) - (\frac{d}{2}) < 1^{st} (X) \land 1^{st} (X) < 1^{st} (X) + (\frac{d}{2})))$
60	25 27 59	syl2anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) \in (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \leftrightarrow (1^{st} (X) \in ℝ^{*} \land 1^{st} (X) - (\frac{d}{2}) < 1^{st} (X) \land 1^{st} (X) < 1^{st} (X) + (\frac{d}{2})))$
61	55 57 58 60	mpbir3and	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) \in (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2}))$
62	31	rexrd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) \in ℝ^{*}$
63	31 56	ltsubrpd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) - (\frac{d}{2}) < 2^{nd} (X)$
64	31 56	ltaddrpd	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) < 2^{nd} (X) + (\frac{d}{2})$
65		elioo1	$⊢ (2^{nd} (X) - (\frac{d}{2}) \in ℝ^{} \land 2^{nd} (X) + (\frac{d}{2}) \in ℝ^{}) \to (2^{nd} (X) \in (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \leftrightarrow (2^{nd} (X) \in ℝ^{*} \land 2^{nd} (X) - (\frac{d}{2}) < 2^{nd} (X) \land 2^{nd} (X) < 2^{nd} (X) + (\frac{d}{2})))$
66	33 35 65	syl2anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (2^{nd} (X) \in (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \leftrightarrow (2^{nd} (X) \in ℝ^{*} \land 2^{nd} (X) - (\frac{d}{2}) < 2^{nd} (X) \land 2^{nd} (X) < 2^{nd} (X) + (\frac{d}{2})))$
67	62 63 64 66	mpbir3and	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) \in (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))$
68	61 67	jca	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) \in (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \land 2^{nd} (X) \in (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))$
69		elxp7	$⊢ X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \leftrightarrow (X \in (V \times V) \land (1^{st} (X) \in (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \land 2^{nd} (X) \in (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))))$
70	54 68 69	sylanbrc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))$
71	70	ralrimiva	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \forall d \in ℝ^{+} X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))$
72		mnfle	$⊢ 1^{st} (X) - (\frac{d}{2}) \in ℝ^{*} \to −∞ \leq 1^{st} (X) - (\frac{d}{2})$
73	25 72	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to −∞ \leq 1^{st} (X) - (\frac{d}{2})$
74		pnfge	$⊢ 1^{st} (X) + (\frac{d}{2}) \in ℝ^{*} \to 1^{st} (X) + (\frac{d}{2}) \leq +∞$
75	27 74	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 1^{st} (X) + (\frac{d}{2}) \leq +∞$
76		mnfxr	$⊢ −∞ \in ℝ^{*}$
77		pnfxr	$⊢ +∞ \in ℝ^{*}$
78		ioossioo	$⊢ ((−∞ \in ℝ^{} \land +∞ \in ℝ^{}) \land (−∞ \leq 1^{st} (X) - (\frac{d}{2}) \land 1^{st} (X) + (\frac{d}{2}) \leq +∞)) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
79	76 77 78	mpanl12	$⊢ (−∞ \leq 1^{st} (X) - (\frac{d}{2}) \land 1^{st} (X) + (\frac{d}{2}) \leq +∞) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
80	73 75 79	syl2anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
81		ioomax	$⊢ (−∞, +∞) = ℝ$
82	80 81	sseqtrdi	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \subseteq ℝ$
83		mnfle	$⊢ 2^{nd} (X) - (\frac{d}{2}) \in ℝ^{*} \to −∞ \leq 2^{nd} (X) - (\frac{d}{2})$
84	33 83	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to −∞ \leq 2^{nd} (X) - (\frac{d}{2})$
85		pnfge	$⊢ 2^{nd} (X) + (\frac{d}{2}) \in ℝ^{*} \to 2^{nd} (X) + (\frac{d}{2}) \leq +∞$
86	35 85	syl	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to 2^{nd} (X) + (\frac{d}{2}) \leq +∞$
87		ioossioo	$⊢ ((−∞ \in ℝ^{} \land +∞ \in ℝ^{}) \land (−∞ \leq 2^{nd} (X) - (\frac{d}{2}) \land 2^{nd} (X) + (\frac{d}{2}) \leq +∞)) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
88	76 77 87	mpanl12	$⊢ (−∞ \leq 2^{nd} (X) - (\frac{d}{2}) \land 2^{nd} (X) + (\frac{d}{2}) \leq +∞) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
89	84 86 88	syl2anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq (−∞, +∞)$
90	89 81	sseqtrdi	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq ℝ$
91		xpss12	$⊢ ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \subseteq ℝ \land (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq ℝ) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq ℝ^{2}$
92	82 90 91	syl2anc	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq ℝ^{2}$
93	92	sselda	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))) \to x \in ℝ^{2}$
94	93	expcom	$⊢ x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to x \in ℝ^{2})$
95	94	ancld	$⊢ x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}))$
96	95	imdistanri	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))) \to ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))))$
97	15	adantr	$⊢ (A \in (J \times_{t} J) \land (X \in A \land d \in ℝ^{+} \land x \in ℝ^{2})) \to A \subseteq ℝ^{2}$
98		simpr1	$⊢ (A \in (J \times_{t} J) \land (X \in A \land d \in ℝ^{+} \land x \in ℝ^{2})) \to X \in A$
99	97 98	sseldd	$⊢ (A \in (J \times_{t} J) \land (X \in A \land d \in ℝ^{+} \land x \in ℝ^{2})) \to X \in ℝ^{2}$
100	99	3anassrs	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to X \in ℝ^{2}$
101		simpr	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to x \in ℝ^{2}$
102		simplr	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to d \in ℝ^{+}$
103	102	rphalfcld	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to \frac{d}{2} \in ℝ^{+}$
104	2	cnre2csqima	$⊢ (X \in ℝ^{2} \land x \in ℝ^{2} \land \frac{d}{2} \in ℝ^{+}) \to (x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to (\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2}))$
105	100 101 103 104	syl3anc	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to (\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2}))$
106		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
107	2 1 106	cnrehmeo	$⊢ G \in ((J \times_{t} J) Homeo TopOpen (ℂ_{fld}))$
108	106	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
109	108	toponunii	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
110	14 109	hmeof1o	$⊢ G \in ((J \times_{t} J) Homeo TopOpen (ℂ_{fld})) \to G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ$
111		f1of	$⊢ G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to G : ℝ^{2} ⟶ ℂ$
112	107 110 111	mp2b	$⊢ G : ℝ^{2} ⟶ ℂ$
113	112	a1i	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G : ℝ^{2} ⟶ ℂ$
114	113 100	ffvelrnd	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G (X) \in ℂ$
115	112	a1i	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to G : ℝ^{2} ⟶ ℂ$
116	115	ffvelrnda	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G (x) \in ℂ$
117		sqsscirc2	$⊢ ((G (X) \in ℂ \land G (x) \in ℂ) \land d \in ℝ^{+}) \to ((\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2}) \to \|G (x) - G (X)\| < d)$
118	114 116 102 117	syl21anc	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to ((\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2}) \to \|G (x) - G (X)\| < d)$
119	118	imp	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land (\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2})) \to \|G (x) - G (X)\| < d$
120	102	rpxrd	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to d \in ℝ^{*}$
121	120	adantr	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to d \in ℝ^{*}$
122		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
123	121 122	jctil	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to (abs \circ - \in ∞Met (ℂ) \land d \in ℝ^{*})$
124	114	adantr	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to G (X) \in ℂ$
125	116	adantr	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to G (x) \in ℂ$
126	124 125	jca	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to (G (X) \in ℂ \land G (x) \in ℂ)$
127		eqid	$⊢ abs \circ - = abs \circ -$
128	127	cnmetdval	$⊢ (G (x) \in ℂ \land G (X) \in ℂ) \to G (x) (abs \circ -) G (X) = \|G (x) - G (X)\|$
129	125 124 128	syl2anc	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to G (x) (abs \circ -) G (X) = \|G (x) - G (X)\|$
130		simpr	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to \|G (x) - G (X)\| < d$
131	129 130	eqbrtrd	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to G (x) (abs \circ -) G (X) < d$
132		elbl3	$⊢ ((abs \circ - \in ∞Met (ℂ) \land d \in ℝ^{*}) \land (G (X) \in ℂ \land G (x) \in ℂ)) \to (G (x) \in (G (X) ball (abs \circ -) d) \leftrightarrow G (x) (abs \circ -) G (X) < d)$
133	132	biimpar	$⊢ (((abs \circ - \in ∞Met (ℂ) \land d \in ℝ^{*}) \land (G (X) \in ℂ \land G (x) \in ℂ)) \land G (x) (abs \circ -) G (X) < d) \to G (x) \in (G (X) ball (abs \circ -) d)$
134	123 126 131 133	syl21anc	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land \|G (x) - G (X)\| < d) \to G (x) \in (G (X) ball (abs \circ -) d)$
135	119 134	syldan	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land (\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2})) \to G (x) \in (G (X) ball (abs \circ -) d)$
136	135	ex	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to ((\|ℜ (G (x) - G (X))\| < \frac{d}{2} \land \|ℑ (G (x) - G (X))\| < \frac{d}{2}) \to G (x) \in (G (X) ball (abs \circ -) d))$
137	105 136	syld	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to G (x) \in (G (X) ball (abs \circ -) d))$
138		f1ocnv	$⊢ G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to G^{-1} : ℂ \underset{1-1 onto}{⟶} ℝ^{2}$
139	107 110 138	mp2b	$⊢ G^{-1} : ℂ \underset{1-1 onto}{⟶} ℝ^{2}$
140		f1ofun	$⊢ G^{-1} : ℂ \underset{1-1 onto}{⟶} ℝ^{2} \to Fun G^{-1}$
141	139 140	ax-mp	$⊢ Fun G^{-1}$
142		f1odm	$⊢ G^{-1} : ℂ \underset{1-1 onto}{⟶} ℝ^{2} \to dom G^{-1} = ℂ$
143	139 142	ax-mp	$⊢ dom G^{-1} = ℂ$
144	116 143	eleqtrrdi	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G (x) \in dom G^{-1}$
145		funfvima	$⊢ (Fun G^{-1} \land G (x) \in dom G^{-1}) \to (G (x) \in (G (X) ball (abs \circ -) d) \to G^{-1} (G (x)) \in G^{-1} [G (X) ball (abs \circ -) d])$
146	141 144 145	sylancr	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (G (x) \in (G (X) ball (abs \circ -) d) \to G^{-1} (G (x)) \in G^{-1} [G (X) ball (abs \circ -) d])$
147	107 110	mp1i	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ$
148		f1ocnvfv1	$⊢ (G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \land x \in ℝ^{2}) \to G^{-1} (G (x)) = x$
149	147 101 148	syl2anc	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to G^{-1} (G (x)) = x$
150	149	eleq1d	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (G^{-1} (G (x)) \in G^{-1} [G (X) ball (abs \circ -) d] \leftrightarrow x \in G^{-1} [G (X) ball (abs \circ -) d])$
151	150	biimpd	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (G^{-1} (G (x)) \in G^{-1} [G (X) ball (abs \circ -) d] \to x \in G^{-1} [G (X) ball (abs \circ -) d])$
152	137 146 151	3syld	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \to (x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to x \in G^{-1} [G (X) ball (abs \circ -) d])$
153	152	imp	$⊢ ((((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ℝ^{2}) \land x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))) \to x \in G^{-1} [G (X) ball (abs \circ -) d]$
154	96 153	syl	$⊢ (((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \land x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})))) \to x \in G^{-1} [G (X) ball (abs \circ -) d]$
155	154	ex	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (x \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \to x \in G^{-1} [G (X) ball (abs \circ -) d])$
156	155	ssrdv	$⊢ ((A \in (J \times_{t} J) \land X \in A) \land d \in ℝ^{+}) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d]$
157	156	ralrimiva	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \forall d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d]$
158	2	mpofun	$⊢ Fun G$
159	158	a1i	$⊢ (A \in (J \times_{t} J) \land X \in A) \to Fun G$
160	15	sselda	$⊢ (A \in (J \times_{t} J) \land X \in A) \to X \in ℝ^{2}$
161		f1odm	$⊢ G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to dom G = ℝ^{2}$
162	107 110 161	mp2b	$⊢ dom G = ℝ^{2}$
163	160 162	eleqtrrdi	$⊢ (A \in (J \times_{t} J) \land X \in A) \to X \in dom G$
164		simpr	$⊢ (A \in (J \times_{t} J) \land X \in A) \to X \in A$
165		funfvima	$⊢ (Fun G \land X \in dom G) \to (X \in A \to G (X) \in G [A])$
166	165	imp	$⊢ ((Fun G \land X \in dom G) \land X \in A) \to G (X) \in G [A]$
167	159 163 164 166	syl21anc	$⊢ (A \in (J \times_{t} J) \land X \in A) \to G (X) \in G [A]$
168		hmeoima	$⊢ (G \in ((J \times_{t} J) Homeo TopOpen (ℂ_{fld})) \land A \in (J \times_{t} J)) \to G [A] \in TopOpen (ℂ_{fld})$
169	107 168	mpan	$⊢ A \in (J \times_{t} J) \to G [A] \in TopOpen (ℂ_{fld})$
170	106	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
171	170	elmopn2	$⊢ abs \circ - \in ∞Met (ℂ) \to (G [A] \in TopOpen (ℂ_{fld}) \leftrightarrow (G [A] \subseteq ℂ \land \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A]))$
172	122 171	ax-mp	$⊢ G [A] \in TopOpen (ℂ_{fld}) \leftrightarrow (G [A] \subseteq ℂ \land \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A])$
173	172	simprbi	$⊢ G [A] \in TopOpen (ℂ_{fld}) \to \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A]$
174	169 173	syl	$⊢ A \in (J \times_{t} J) \to \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A]$
175	174	adantr	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A]$
176		oveq1	$⊢ m = G (X) \to m ball (abs \circ -) d = G (X) ball (abs \circ -) d$
177	176	sseq1d	$⊢ m = G (X) \to (m ball (abs \circ -) d \subseteq G [A] \leftrightarrow G (X) ball (abs \circ -) d \subseteq G [A])$
178	177	rexbidv	$⊢ m = G (X) \to (\exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A] \leftrightarrow \exists d \in ℝ^{+} G (X) ball (abs \circ -) d \subseteq G [A])$
179	178	rspcva	$⊢ (G (X) \in G [A] \land \forall m \in G [A] \exists d \in ℝ^{+} m ball (abs \circ -) d \subseteq G [A]) \to \exists d \in ℝ^{+} G (X) ball (abs \circ -) d \subseteq G [A]$
180	167 175 179	syl2anc	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} G (X) ball (abs \circ -) d \subseteq G [A]$
181		imass2	$⊢ G (X) ball (abs \circ -) d \subseteq G [A] \to G^{-1} [G (X) ball (abs \circ -) d] \subseteq G^{-1} [G [A]]$
182		f1of1	$⊢ G : ℝ^{2} \underset{1-1 onto}{⟶} ℂ \to G : ℝ^{2} \underset{1-1}{⟶} ℂ$
183	107 110 182	mp2b	$⊢ G : ℝ^{2} \underset{1-1}{⟶} ℂ$
184		f1imacnv	$⊢ (G : ℝ^{2} \underset{1-1}{⟶} ℂ \land A \subseteq ℝ^{2}) \to G^{-1} [G [A]] = A$
185	183 15 184	sylancr	$⊢ A \in (J \times_{t} J) \to G^{-1} [G [A]] = A$
186	185	sseq2d	$⊢ A \in (J \times_{t} J) \to (G^{-1} [G (X) ball (abs \circ -) d] \subseteq G^{-1} [G [A]] \leftrightarrow G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
187	181 186	syl5ib	$⊢ A \in (J \times_{t} J) \to (G (X) ball (abs \circ -) d \subseteq G [A] \to G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
188	187	reximdv	$⊢ A \in (J \times_{t} J) \to (\exists d \in ℝ^{+} G (X) ball (abs \circ -) d \subseteq G [A] \to \exists d \in ℝ^{+} G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
189	188	adantr	$⊢ (A \in (J \times_{t} J) \land X \in A) \to (\exists d \in ℝ^{+} G (X) ball (abs \circ -) d \subseteq G [A] \to \exists d \in ℝ^{+} G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
190	180 189	mpd	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} G^{-1} [G (X) ball (abs \circ -) d] \subseteq A$
191		r19.29	$⊢ (\forall d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d] \land \exists d \in ℝ^{+} G^{-1} [G (X) ball (abs \circ -) d] \subseteq A) \to \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d] \land G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
192	157 190 191	syl2anc	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d] \land G^{-1} [G (X) ball (abs \circ -) d] \subseteq A)$
193		sstr	$⊢ ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d] \land G^{-1} [G (X) ball (abs \circ -) d] \subseteq A) \to (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A$
194	193	reximi	$⊢ \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq G^{-1} [G (X) ball (abs \circ -) d] \land G^{-1} [G (X) ball (abs \circ -) d] \subseteq A) \to \exists d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A$
195	192 194	syl	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A$
196		r19.29	$⊢ (\forall d \in ℝ^{+} X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land \exists d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A) \to \exists d \in ℝ^{+} (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)$
197	71 195 196	syl2anc	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)$
198		r19.29	$⊢ (\forall d \in ℝ^{+} (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B \land \exists d \in ℝ^{+} (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)) \to \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B \land (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A))$
199	52 197 198	syl2anc	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B \land (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A))$
200		eleq2	$⊢ r = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \to (X \in r \leftrightarrow X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))))$
201		sseq1	$⊢ r = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \to (r \subseteq A \leftrightarrow (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)$
202	200 201	anbi12d	$⊢ r = (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \to ((X \in r \land r \subseteq A) \leftrightarrow (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A))$
203	202	rspcev	$⊢ ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B \land (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)) \to \exists r \in B (X \in r \land r \subseteq A)$
204	203	rexlimivw	$⊢ \exists d \in ℝ^{+} ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \in B \land (X \in ((1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2}))) \land (1^{st} (X) - (\frac{d}{2}), 1^{st} (X) + (\frac{d}{2})) \times (2^{nd} (X) - (\frac{d}{2}), 2^{nd} (X) + (\frac{d}{2})) \subseteq A)) \to \exists r \in B (X \in r \land r \subseteq A)$
205	199 204	syl	$⊢ (A \in (J \times_{t} J) \land X \in A) \to \exists r \in B (X \in r \land r \subseteq A)$

Metamath Proof Explorer

Theorem tpr2rico

Proof