Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tpr2rico Structured version   Visualization version   GIF version

Theorem tpr2rico 31904
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.
StepHypRef Expression
1 df-ioo 13126 . . . . . . . . . 10 (,) = (π‘₯ ∈ ℝ*, 𝑦 ∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (π‘₯ < 𝑧 ∧ 𝑧 < 𝑦)})
21ixxf 13132 . . . . . . . . 9 (,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ*
3 ffn 6627 . . . . . . . . 9 ((,):(ℝ* Γ— ℝ*)βŸΆπ’« ℝ* β†’ (,) Fn (ℝ* Γ— ℝ*))
42, 3mp1i 13 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (,) Fn (ℝ* Γ— ℝ*))
5 elssuni 4878 . . . . . . . . . . . . . 14 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ 𝐴 βŠ† βˆͺ (𝐽 Γ—t 𝐽))
6 tpr2rico.0 . . . . . . . . . . . . . . . 16 𝐽 = (topGenβ€˜ran (,))
7 retop 23967 . . . . . . . . . . . . . . . 16 (topGenβ€˜ran (,)) ∈ Top
86, 7eqeltri 2833 . . . . . . . . . . . . . . 15 𝐽 ∈ Top
9 uniretop 23968 . . . . . . . . . . . . . . . 16 ℝ = βˆͺ (topGenβ€˜ran (,))
106unieqi 4858 . . . . . . . . . . . . . . . 16 βˆͺ 𝐽 = βˆͺ (topGenβ€˜ran (,))
119, 10eqtr4i 2767 . . . . . . . . . . . . . . 15 ℝ = βˆͺ 𝐽
128, 8, 11, 11txunii 22786 . . . . . . . . . . . . . 14 (ℝ Γ— ℝ) = βˆͺ (𝐽 Γ—t 𝐽)
135, 12sseqtrrdi 3978 . . . . . . . . . . . . 13 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ 𝐴 βŠ† (ℝ Γ— ℝ))
1413ad2antrr 724 . . . . . . . . . . . 12 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝐴 βŠ† (ℝ Γ— ℝ))
15 simplr 767 . . . . . . . . . . . 12 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑋 ∈ 𝐴)
1614, 15sseldd 3928 . . . . . . . . . . 11 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑋 ∈ (ℝ Γ— ℝ))
17 xp1st 7892 . . . . . . . . . . 11 (𝑋 ∈ (ℝ Γ— ℝ) β†’ (1st β€˜π‘‹) ∈ ℝ)
1816, 17syl 17 . . . . . . . . . 10 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (1st β€˜π‘‹) ∈ ℝ)
19 simpr 486 . . . . . . . . . . . 12 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑑 ∈ ℝ+)
2019rpred 12815 . . . . . . . . . . 11 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑑 ∈ ℝ)
2120rehalfcld 12263 . . . . . . . . . 10 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (𝑑 / 2) ∈ ℝ)
2218, 21resubcld 11446 . . . . . . . . 9 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ)
2322rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ*)
2418, 21readdcld 11047 . . . . . . . . 9 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ)
2524rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*)
26 fnovrn 7476 . . . . . . . 8 (((,) Fn (ℝ* Γ— ℝ*) ∧ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* ∧ ((1st β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,))
274, 23, 25, 26syl3anc 1371 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,))
28 xp2nd 7893 . . . . . . . . . . 11 (𝑋 ∈ (ℝ Γ— ℝ) β†’ (2nd β€˜π‘‹) ∈ ℝ)
2916, 28syl 17 . . . . . . . . . 10 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (2nd β€˜π‘‹) ∈ ℝ)
3029, 21resubcld 11446 . . . . . . . . 9 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ)
3130rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ*)
3229, 21readdcld 11047 . . . . . . . . 9 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ)
3332rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*)
34 fnovrn 7476 . . . . . . . 8 (((,) Fn (ℝ* Γ— ℝ*) ∧ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* ∧ ((2nd β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,))
354, 31, 33, 34syl3anc 1371 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,))
36 eqidd 2737 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))))
37 xpeq1 5611 . . . . . . . . 9 (π‘₯ = (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) β†’ (π‘₯ Γ— 𝑦) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— 𝑦))
3837eqeq2d 2747 . . . . . . . 8 (π‘₯ = (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) β†’ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = (π‘₯ Γ— 𝑦) ↔ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— 𝑦)))
39 xpeq2 5618 . . . . . . . . 9 (𝑦 = (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— 𝑦) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))))
4039eqeq2d 2747 . . . . . . . 8 (𝑦 = (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) β†’ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— 𝑦) ↔ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))))
4138, 40rspc2ev 3578 . . . . . . 7 (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,) ∧ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) ∈ ran (,) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))) β†’ βˆƒπ‘₯ ∈ ran (,)βˆƒπ‘¦ ∈ ran (,)((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = (π‘₯ Γ— 𝑦))
4227, 35, 36, 41syl3anc 1371 . . . . . 6 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ βˆƒπ‘₯ ∈ ran (,)βˆƒπ‘¦ ∈ ran (,)((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = (π‘₯ Γ— 𝑦))
43 eqid 2736 . . . . . . 7 (π‘₯ ∈ ran (,), 𝑦 ∈ ran (,) ↦ (π‘₯ Γ— 𝑦)) = (π‘₯ ∈ ran (,), 𝑦 ∈ ran (,) ↦ (π‘₯ Γ— 𝑦))
44 vex 3442 . . . . . . . 8 π‘₯ ∈ V
45 vex 3442 . . . . . . . 8 𝑦 ∈ V
4644, 45xpex 7632 . . . . . . 7 (π‘₯ Γ— 𝑦) ∈ V
4743, 46elrnmpo 7439 . . . . . 6 (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ ran (π‘₯ ∈ ran (,), 𝑦 ∈ ran (,) ↦ (π‘₯ Γ— 𝑦)) ↔ βˆƒπ‘₯ ∈ ran (,)βˆƒπ‘¦ ∈ ran (,)((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) = (π‘₯ Γ— 𝑦))
4842, 47sylibr 234 . . . . 5 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ ran (π‘₯ ∈ ran (,), 𝑦 ∈ ran (,) ↦ (π‘₯ Γ— 𝑦)))
49 tpr2rico.2 . . . . 5 𝐡 = ran (π‘₯ ∈ ran (,), 𝑦 ∈ ran (,) ↦ (π‘₯ Γ— 𝑦))
5048, 49eleqtrrdi 2848 . . . 4 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡)
5150ralrimiva 3140 . . 3 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆ€π‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡)
52 xpss 5613 . . . . . . 7 (ℝ Γ— ℝ) βŠ† (V Γ— V)
5352, 16sselid 3925 . . . . . 6 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑋 ∈ (V Γ— V))
5418rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (1st β€˜π‘‹) ∈ ℝ*)
5519rphalfcld 12827 . . . . . . . . 9 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (𝑑 / 2) ∈ ℝ+)
5618, 55ltsubrpd 12847 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) < (1st β€˜π‘‹))
5718, 55ltaddrpd 12848 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (1st β€˜π‘‹) < ((1st β€˜π‘‹) + (𝑑 / 2)))
58 elioo1 13162 . . . . . . . . 9 ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* ∧ ((1st β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*) β†’ ((1st β€˜π‘‹) ∈ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ↔ ((1st β€˜π‘‹) ∈ ℝ* ∧ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) < (1st β€˜π‘‹) ∧ (1st β€˜π‘‹) < ((1st β€˜π‘‹) + (𝑑 / 2)))))
5923, 25, 58syl2anc 585 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) ∈ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ↔ ((1st β€˜π‘‹) ∈ ℝ* ∧ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) < (1st β€˜π‘‹) ∧ (1st β€˜π‘‹) < ((1st β€˜π‘‹) + (𝑑 / 2)))))
6054, 56, 57, 59mpbir3and 1342 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (1st β€˜π‘‹) ∈ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))))
6129rexrd 11068 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (2nd β€˜π‘‹) ∈ ℝ*)
6229, 55ltsubrpd 12847 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) < (2nd β€˜π‘‹))
6329, 55ltaddrpd 12848 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (2nd β€˜π‘‹) < ((2nd β€˜π‘‹) + (𝑑 / 2)))
64 elioo1 13162 . . . . . . . . 9 ((((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* ∧ ((2nd β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ*) β†’ ((2nd β€˜π‘‹) ∈ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) ↔ ((2nd β€˜π‘‹) ∈ ℝ* ∧ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) < (2nd β€˜π‘‹) ∧ (2nd β€˜π‘‹) < ((2nd β€˜π‘‹) + (𝑑 / 2)))))
6531, 33, 64syl2anc 585 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) ∈ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) ↔ ((2nd β€˜π‘‹) ∈ ℝ* ∧ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) < (2nd β€˜π‘‹) ∧ (2nd β€˜π‘‹) < ((2nd β€˜π‘‹) + (𝑑 / 2)))))
6661, 62, 63, 65mpbir3and 1342 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (2nd β€˜π‘‹) ∈ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))
6760, 66jca 513 . . . . . 6 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) ∈ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ∧ (2nd β€˜π‘‹) ∈ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))))
68 elxp7 7895 . . . . . 6 (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ↔ (𝑋 ∈ (V Γ— V) ∧ ((1st β€˜π‘‹) ∈ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) ∧ (2nd β€˜π‘‹) ∈ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))))
6953, 67, 68sylanbrc 584 . . . . 5 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))))
7069ralrimiva 3140 . . . 4 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆ€π‘‘ ∈ ℝ+ 𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))))
71 mnfle 12913 . . . . . . . . . . . . . . . . . 18 (((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* β†’ -∞ ≀ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)))
7223, 71syl 17 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ -∞ ≀ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)))
73 pnfge 12909 . . . . . . . . . . . . . . . . . 18 (((1st β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ* β†’ ((1st β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)
7425, 73syl 17 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((1st β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)
75 mnfxr 11075 . . . . . . . . . . . . . . . . . 18 -∞ ∈ ℝ*
76 pnfxr 11072 . . . . . . . . . . . . . . . . . 18 +∞ ∈ ℝ*
77 ioossioo 13216 . . . . . . . . . . . . . . . . . 18 (((-∞ ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≀ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∧ ((1st β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
7875, 76, 77mpanl12 700 . . . . . . . . . . . . . . . . 17 ((-∞ ≀ ((1st β€˜π‘‹) βˆ’ (𝑑 / 2)) ∧ ((1st β€˜π‘‹) + (𝑑 / 2)) ≀ +∞) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
7972, 74, 78syl2anc 585 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
80 ioomax 13197 . . . . . . . . . . . . . . . 16 (-∞(,)+∞) = ℝ
8179, 80sseqtrdi 3977 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) βŠ† ℝ)
82 mnfle 12913 . . . . . . . . . . . . . . . . . 18 (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∈ ℝ* β†’ -∞ ≀ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)))
8331, 82syl 17 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ -∞ ≀ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)))
84 pnfge 12909 . . . . . . . . . . . . . . . . . 18 (((2nd β€˜π‘‹) + (𝑑 / 2)) ∈ ℝ* β†’ ((2nd β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)
8533, 84syl 17 . . . . . . . . . . . . . . . . 17 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((2nd β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)
86 ioossioo 13216 . . . . . . . . . . . . . . . . . 18 (((-∞ ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ (-∞ ≀ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∧ ((2nd β€˜π‘‹) + (𝑑 / 2)) ≀ +∞)) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
8775, 76, 86mpanl12 700 . . . . . . . . . . . . . . . . 17 ((-∞ ≀ ((2nd β€˜π‘‹) βˆ’ (𝑑 / 2)) ∧ ((2nd β€˜π‘‹) + (𝑑 / 2)) ≀ +∞) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
8883, 85, 87syl2anc 585 . . . . . . . . . . . . . . . 16 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) βŠ† (-∞(,)+∞))
8988, 80sseqtrdi 3977 . . . . . . . . . . . . . . 15 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) βŠ† ℝ)
90 xpss12 5612 . . . . . . . . . . . . . . 15 (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) βŠ† ℝ ∧ (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))) βŠ† ℝ) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (ℝ Γ— ℝ))
9181, 89, 90syl2anc 585 . . . . . . . . . . . . . 14 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (ℝ Γ— ℝ))
9291sselda 3927 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))) β†’ π‘₯ ∈ (ℝ Γ— ℝ))
9392expcom 415 . . . . . . . . . . . 12 (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ π‘₯ ∈ (ℝ Γ— ℝ)))
9493ancld 552 . . . . . . . . . . 11 (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ))))
9594imdistanri 571 . . . . . . . . . 10 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))) β†’ ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))))
9613adantr 482 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ+ ∧ π‘₯ ∈ (ℝ Γ— ℝ))) β†’ 𝐴 βŠ† (ℝ Γ— ℝ))
97 simpr1 1194 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ+ ∧ π‘₯ ∈ (ℝ Γ— ℝ))) β†’ 𝑋 ∈ 𝐴)
9896, 97sseldd 3928 . . . . . . . . . . . . . . 15 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ (𝑋 ∈ 𝐴 ∧ 𝑑 ∈ ℝ+ ∧ π‘₯ ∈ (ℝ Γ— ℝ))) β†’ 𝑋 ∈ (ℝ Γ— ℝ))
99983anassrs 1360 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ 𝑋 ∈ (ℝ Γ— ℝ))
100 simpr 486 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ π‘₯ ∈ (ℝ Γ— ℝ))
101 simplr 767 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ 𝑑 ∈ ℝ+)
102101rphalfcld 12827 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (𝑑 / 2) ∈ ℝ+)
103 tpr2rico.1 . . . . . . . . . . . . . . 15 𝐺 = (𝑒 ∈ ℝ, 𝑣 ∈ ℝ ↦ (𝑒 + (i Β· 𝑣)))
104103cnre2csqima 31903 . . . . . . . . . . . . . 14 ((𝑋 ∈ (ℝ Γ— ℝ) ∧ π‘₯ ∈ (ℝ Γ— ℝ) ∧ (𝑑 / 2) ∈ ℝ+) β†’ (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ ((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2))))
10599, 100, 102, 104syl3anc 1371 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ ((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2))))
106 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
107103, 6, 106cnrehmeo 24158 . . . . . . . . . . . . . . . . . . . 20 𝐺 ∈ ((𝐽 Γ—t 𝐽)Homeo(TopOpenβ€˜β„‚fld))
108106cnfldtopon 23988 . . . . . . . . . . . . . . . . . . . . . 22 (TopOpenβ€˜β„‚fld) ∈ (TopOnβ€˜β„‚)
109108toponunii 22107 . . . . . . . . . . . . . . . . . . . . 21 β„‚ = βˆͺ (TopOpenβ€˜β„‚fld)
11012, 109hmeof1o 22957 . . . . . . . . . . . . . . . . . . . 20 (𝐺 ∈ ((𝐽 Γ—t 𝐽)Homeo(TopOpenβ€˜β„‚fld)) β†’ 𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚)
111 f1of 6743 . . . . . . . . . . . . . . . . . . . 20 (𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚ β†’ 𝐺:(ℝ Γ— ℝ)βŸΆβ„‚)
112107, 110, 111mp2b 10 . . . . . . . . . . . . . . . . . . 19 𝐺:(ℝ Γ— ℝ)βŸΆβ„‚
113112a1i 11 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ 𝐺:(ℝ Γ— ℝ)βŸΆβ„‚)
114113, 99ffvelcdmd 6991 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (πΊβ€˜π‘‹) ∈ β„‚)
115112a1i 11 . . . . . . . . . . . . . . . . . 18 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ 𝐺:(ℝ Γ— ℝ)βŸΆβ„‚)
116115ffvelcdmda 6990 . . . . . . . . . . . . . . . . 17 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
117 sqsscirc2 31901 . . . . . . . . . . . . . . . . 17 ((((πΊβ€˜π‘‹) ∈ β„‚ ∧ (πΊβ€˜π‘₯) ∈ β„‚) ∧ 𝑑 ∈ ℝ+) β†’ (((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2)) β†’ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑))
118114, 116, 101, 117syl21anc 836 . . . . . . . . . . . . . . . 16 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2)) β†’ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑))
119118imp 408 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ ((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2))) β†’ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑)
120101rpxrd 12816 . . . . . . . . . . . . . . . . . 18 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ 𝑑 ∈ ℝ*)
121120adantr 482 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ 𝑑 ∈ ℝ*)
122 cnxmet 23978 . . . . . . . . . . . . . . . . 17 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
123121, 122jctil 521 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ ((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝑑 ∈ ℝ*))
124114adantr 482 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ (πΊβ€˜π‘‹) ∈ β„‚)
125116adantr 482 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
126124, 125jca 513 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ ((πΊβ€˜π‘‹) ∈ β„‚ ∧ (πΊβ€˜π‘₯) ∈ β„‚))
127 eqid 2736 . . . . . . . . . . . . . . . . . . 19 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
128127cnmetdval 23976 . . . . . . . . . . . . . . . . . 18 (((πΊβ€˜π‘₯) ∈ β„‚ ∧ (πΊβ€˜π‘‹) ∈ β„‚) β†’ ((πΊβ€˜π‘₯)(abs ∘ βˆ’ )(πΊβ€˜π‘‹)) = (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))))
129125, 124, 128syl2anc 585 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ ((πΊβ€˜π‘₯)(abs ∘ βˆ’ )(πΊβ€˜π‘‹)) = (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))))
130 simpr 486 . . . . . . . . . . . . . . . . 17 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑)
131129, 130eqbrtrd 5104 . . . . . . . . . . . . . . . 16 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ ((πΊβ€˜π‘₯)(abs ∘ βˆ’ )(πΊβ€˜π‘‹)) < 𝑑)
132 elbl3 23587 . . . . . . . . . . . . . . . . 17 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝑑 ∈ ℝ*) ∧ ((πΊβ€˜π‘‹) ∈ β„‚ ∧ (πΊβ€˜π‘₯) ∈ β„‚)) β†’ ((πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) ↔ ((πΊβ€˜π‘₯)(abs ∘ βˆ’ )(πΊβ€˜π‘‹)) < 𝑑))
133132biimpar 479 . . . . . . . . . . . . . . . 16 (((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝑑 ∈ ℝ*) ∧ ((πΊβ€˜π‘‹) ∈ β„‚ ∧ (πΊβ€˜π‘₯) ∈ β„‚)) ∧ ((πΊβ€˜π‘₯)(abs ∘ βˆ’ )(πΊβ€˜π‘‹)) < 𝑑) β†’ (πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))
134123, 126, 131, 133syl21anc 836 . . . . . . . . . . . . . . 15 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ (absβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹))) < 𝑑) β†’ (πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))
135119, 134syldan 592 . . . . . . . . . . . . . 14 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ ((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2))) β†’ (πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))
136135ex 414 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (((absβ€˜(β„œβ€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2) ∧ (absβ€˜(β„‘β€˜((πΊβ€˜π‘₯) βˆ’ (πΊβ€˜π‘‹)))) < (𝑑 / 2)) β†’ (πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
137105, 136syld 47 . . . . . . . . . . . 12 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ (πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
138 f1ocnv 6755 . . . . . . . . . . . . . . 15 (𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚ β†’ ◑𝐺:ℂ–1-1-ontoβ†’(ℝ Γ— ℝ))
139107, 110, 138mp2b 10 . . . . . . . . . . . . . 14 ◑𝐺:ℂ–1-1-ontoβ†’(ℝ Γ— ℝ)
140 f1ofun 6745 . . . . . . . . . . . . . 14 (◑𝐺:ℂ–1-1-ontoβ†’(ℝ Γ— ℝ) β†’ Fun ◑𝐺)
141139, 140ax-mp 5 . . . . . . . . . . . . 13 Fun ◑𝐺
142 f1odm 6747 . . . . . . . . . . . . . . 15 (◑𝐺:ℂ–1-1-ontoβ†’(ℝ Γ— ℝ) β†’ dom ◑𝐺 = β„‚)
143139, 142ax-mp 5 . . . . . . . . . . . . . 14 dom ◑𝐺 = β„‚
144116, 143eleqtrrdi 2848 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (πΊβ€˜π‘₯) ∈ dom ◑𝐺)
145 funfvima 7135 . . . . . . . . . . . . 13 ((Fun ◑𝐺 ∧ (πΊβ€˜π‘₯) ∈ dom ◑𝐺) β†’ ((πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) β†’ (β—‘πΊβ€˜(πΊβ€˜π‘₯)) ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
146141, 144, 145sylancr 588 . . . . . . . . . . . 12 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ ((πΊβ€˜π‘₯) ∈ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) β†’ (β—‘πΊβ€˜(πΊβ€˜π‘₯)) ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
147107, 110mp1i 13 . . . . . . . . . . . . . . 15 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ 𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚)
148 f1ocnvfv1 7177 . . . . . . . . . . . . . . 15 ((𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚ ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (β—‘πΊβ€˜(πΊβ€˜π‘₯)) = π‘₯)
149147, 100, 148syl2anc 585 . . . . . . . . . . . . . 14 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (β—‘πΊβ€˜(πΊβ€˜π‘₯)) = π‘₯)
150149eleq1d 2821 . . . . . . . . . . . . 13 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ ((β—‘πΊβ€˜(πΊβ€˜π‘₯)) ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ↔ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
151150biimpd 228 . . . . . . . . . . . 12 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ ((β—‘πΊβ€˜(πΊβ€˜π‘₯)) ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) β†’ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
152137, 146, 1513syld 60 . . . . . . . . . . 11 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) β†’ (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
153152imp 408 . . . . . . . . . 10 (((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ (ℝ Γ— ℝ)) ∧ π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))) β†’ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
15495, 153syl 17 . . . . . . . . 9 ((((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) ∧ π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))) β†’ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
155154ex 414 . . . . . . . 8 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ (π‘₯ ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ π‘₯ ∈ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))))
156155ssrdv 3933 . . . . . . 7 (((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) ∧ 𝑑 ∈ ℝ+) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
157156ralrimiva 3140 . . . . . 6 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆ€π‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)))
158103mpofun 7427 . . . . . . . . . 10 Fun 𝐺
159158a1i 11 . . . . . . . . 9 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ Fun 𝐺)
16013sselda 3927 . . . . . . . . . 10 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ 𝑋 ∈ (ℝ Γ— ℝ))
161 f1odm 6747 . . . . . . . . . . 11 (𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚ β†’ dom 𝐺 = (ℝ Γ— ℝ))
162107, 110, 161mp2b 10 . . . . . . . . . 10 dom 𝐺 = (ℝ Γ— ℝ)
163160, 162eleqtrrdi 2848 . . . . . . . . 9 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ 𝑋 ∈ dom 𝐺)
164 simpr 486 . . . . . . . . 9 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ 𝑋 ∈ 𝐴)
165 funfvima 7135 . . . . . . . . . 10 ((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) β†’ (𝑋 ∈ 𝐴 β†’ (πΊβ€˜π‘‹) ∈ (𝐺 β€œ 𝐴)))
166165imp 408 . . . . . . . . 9 (((Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺) ∧ 𝑋 ∈ 𝐴) β†’ (πΊβ€˜π‘‹) ∈ (𝐺 β€œ 𝐴))
167159, 163, 164, 166syl21anc 836 . . . . . . . 8 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ (πΊβ€˜π‘‹) ∈ (𝐺 β€œ 𝐴))
168 hmeoima 22958 . . . . . . . . . . 11 ((𝐺 ∈ ((𝐽 Γ—t 𝐽)Homeo(TopOpenβ€˜β„‚fld)) ∧ 𝐴 ∈ (𝐽 Γ—t 𝐽)) β†’ (𝐺 β€œ 𝐴) ∈ (TopOpenβ€˜β„‚fld))
169107, 168mpan 688 . . . . . . . . . 10 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ (𝐺 β€œ 𝐴) ∈ (TopOpenβ€˜β„‚fld))
170106cnfldtopn 23987 . . . . . . . . . . . . 13 (TopOpenβ€˜β„‚fld) = (MetOpenβ€˜(abs ∘ βˆ’ ))
171170elmopn2 23640 . . . . . . . . . . . 12 ((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) β†’ ((𝐺 β€œ 𝐴) ∈ (TopOpenβ€˜β„‚fld) ↔ ((𝐺 β€œ 𝐴) βŠ† β„‚ ∧ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))))
172122, 171ax-mp 5 . . . . . . . . . . 11 ((𝐺 β€œ 𝐴) ∈ (TopOpenβ€˜β„‚fld) ↔ ((𝐺 β€œ 𝐴) βŠ† β„‚ ∧ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴)))
173172simprbi 498 . . . . . . . . . 10 ((𝐺 β€œ 𝐴) ∈ (TopOpenβ€˜β„‚fld) β†’ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))
174169, 173syl 17 . . . . . . . . 9 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))
175174adantr 482 . . . . . . . 8 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))
176 oveq1 7311 . . . . . . . . . . 11 (π‘š = (πΊβ€˜π‘‹) β†’ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) = ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑))
177176sseq1d 3958 . . . . . . . . . 10 (π‘š = (πΊβ€˜π‘‹) β†’ ((π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) ↔ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴)))
178177rexbidv 3172 . . . . . . . . 9 (π‘š = (πΊβ€˜π‘‹) β†’ (βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) ↔ βˆƒπ‘‘ ∈ ℝ+ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴)))
179178rspcva 3565 . . . . . . . 8 (((πΊβ€˜π‘‹) ∈ (𝐺 β€œ 𝐴) ∧ βˆ€π‘š ∈ (𝐺 β€œ 𝐴)βˆƒπ‘‘ ∈ ℝ+ (π‘š(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴)) β†’ βˆƒπ‘‘ ∈ ℝ+ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))
180167, 175, 179syl2anc 585 . . . . . . 7 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴))
181 imass2 6017 . . . . . . . . . 10 (((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) β†’ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† (◑𝐺 β€œ (𝐺 β€œ 𝐴)))
182 f1of1 6742 . . . . . . . . . . . . 13 (𝐺:(ℝ Γ— ℝ)–1-1-ontoβ†’β„‚ β†’ 𝐺:(ℝ Γ— ℝ)–1-1β†’β„‚)
183107, 110, 182mp2b 10 . . . . . . . . . . . 12 𝐺:(ℝ Γ— ℝ)–1-1β†’β„‚
184 f1imacnv 6759 . . . . . . . . . . . 12 ((𝐺:(ℝ Γ— ℝ)–1-1β†’β„‚ ∧ 𝐴 βŠ† (ℝ Γ— ℝ)) β†’ (◑𝐺 β€œ (𝐺 β€œ 𝐴)) = 𝐴)
185183, 13, 184sylancr 588 . . . . . . . . . . 11 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ (◑𝐺 β€œ (𝐺 β€œ 𝐴)) = 𝐴)
186185sseq2d 3959 . . . . . . . . . 10 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ ((◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† (◑𝐺 β€œ (𝐺 β€œ 𝐴)) ↔ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
187181, 186syl5ib 245 . . . . . . . . 9 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ (((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) β†’ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
188187reximdv 3164 . . . . . . . 8 (𝐴 ∈ (𝐽 Γ—t 𝐽) β†’ (βˆƒπ‘‘ ∈ ℝ+ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
189188adantr 482 . . . . . . 7 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ (βˆƒπ‘‘ ∈ ℝ+ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑) βŠ† (𝐺 β€œ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
190180, 189mpd 15 . . . . . 6 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴)
191 r19.29 3114 . . . . . 6 ((βˆ€π‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ βˆƒπ‘‘ ∈ ℝ+ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
192157, 190, 191syl2anc 585 . . . . 5 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴))
193 sstr 3935 . . . . . 6 ((((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴) β†’ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)
194193reximi 3084 . . . . 5 (βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) ∧ (◑𝐺 β€œ ((πΊβ€˜π‘‹)(ballβ€˜(abs ∘ βˆ’ ))𝑑)) βŠ† 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)
195192, 194syl 17 . . . 4 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)
196 r19.29 3114 . . . 4 ((βˆ€π‘‘ ∈ ℝ+ 𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ βˆƒπ‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴))
19770, 195, 196syl2anc 585 . . 3 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴))
198 r19.29 3114 . . 3 ((βˆ€π‘‘ ∈ ℝ+ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡 ∧ βˆƒπ‘‘ ∈ ℝ+ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)) β†’ βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡 ∧ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)))
19951, 197, 198syl2anc 585 . 2 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡 ∧ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)))
200 eleq2 2825 . . . . 5 (π‘Ÿ = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ (𝑋 ∈ π‘Ÿ ↔ 𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2))))))
201 sseq1 3952 . . . . 5 (π‘Ÿ = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ (π‘Ÿ βŠ† 𝐴 ↔ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴))
202200, 201anbi12d 632 . . . 4 (π‘Ÿ = ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) β†’ ((𝑋 ∈ π‘Ÿ ∧ π‘Ÿ βŠ† 𝐴) ↔ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)))
203202rspcev 3567 . . 3 ((((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡 ∧ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)) β†’ βˆƒπ‘Ÿ ∈ 𝐡 (𝑋 ∈ π‘Ÿ ∧ π‘Ÿ βŠ† 𝐴))
204203rexlimivw 3145 . 2 (βˆƒπ‘‘ ∈ ℝ+ (((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∈ 𝐡 ∧ (𝑋 ∈ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) ∧ ((((1st β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((1st β€˜π‘‹) + (𝑑 / 2))) Γ— (((2nd β€˜π‘‹) βˆ’ (𝑑 / 2))(,)((2nd β€˜π‘‹) + (𝑑 / 2)))) βŠ† 𝐴)) β†’ βˆƒπ‘Ÿ ∈ 𝐡 (𝑋 ∈ π‘Ÿ ∧ π‘Ÿ βŠ† 𝐴))
205199, 204syl 17 1 ((𝐴 ∈ (𝐽 Γ—t 𝐽) ∧ 𝑋 ∈ 𝐴) β†’ βˆƒπ‘Ÿ ∈ 𝐡 (𝑋 ∈ π‘Ÿ ∧ π‘Ÿ βŠ† 𝐴))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  βˆ€wral 3062  βˆƒwrex 3071  Vcvv 3438   βŠ† wss 3893  π’« cpw 4540  βˆͺ cuni 4845   class class class wbr 5082   Γ— cxp 5595  β—‘ccnv 5596  dom cdm 5597  ran crn 5598   β€œ cima 5600   ∘ ccom 5601  Fun wfun 6449   Fn wfn 6450  βŸΆwf 6451  β€“1-1β†’wf1 6452  β€“1-1-ontoβ†’wf1o 6454  β€˜cfv 6455  (class class class)co 7304   ∈ cmpo 7306  1st c1st 7858  2nd c2nd 7859  β„‚cc 10912  β„cr 10913  ici 10916   + caddc 10917   Β· cmul 10919  +∞cpnf 11049  -∞cmnf 11050  β„*cxr 11051   < clt 11052   ≀ cle 11053   βˆ’ cmin 11248   / cdiv 11675  2c2 12071  β„+crp 12773  (,)cioo 13122  β„œcre 14850  β„‘cim 14851  abscabs 14987  TopOpenctopn 17174  topGenctg 17190  βˆžMetcxmet 20624  ballcbl 20626  β„‚fldccnfld 20639  Topctop 22084   Γ—t ctx 22753  Homeochmeo 22946
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-rep 5219  ax-sep 5233  ax-nul 5240  ax-pow 5298  ax-pr 5362  ax-un 7617  ax-cnex 10970  ax-resscn 10971  ax-1cn 10972  ax-icn 10973  ax-addcl 10974  ax-addrcl 10975  ax-mulcl 10976  ax-mulrcl 10977  ax-mulcom 10978  ax-addass 10979  ax-mulass 10980  ax-distr 10981  ax-i2m1 10982  ax-1ne0 10983  ax-1rid 10984  ax-rnegex 10985  ax-rrecex 10986  ax-cnre 10987  ax-pre-lttri 10988  ax-pre-lttrn 10989  ax-pre-ltadd 10990  ax-pre-mulgt0 10991  ax-pre-sup 10992  ax-addf 10993  ax-mulf 10994
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3278  df-reu 3279  df-rab 3280  df-v 3440  df-sbc 3723  df-csb 3839  df-dif 3896  df-un 3898  df-in 3900  df-ss 3910  df-pss 3912  df-nul 4264  df-if 4467  df-pw 4542  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4846  df-int 4888  df-iun 4934  df-iin 4935  df-br 5083  df-opab 5145  df-mpt 5166  df-tr 5200  df-id 5497  df-eprel 5503  df-po 5511  df-so 5512  df-fr 5552  df-se 5553  df-we 5554  df-xp 5603  df-rel 5604  df-cnv 5605  df-co 5606  df-dm 5607  df-rn 5608  df-res 5609  df-ima 5610  df-pred 6214  df-ord 6281  df-on 6282  df-lim 6283  df-suc 6284  df-iota 6407  df-fun 6457  df-fn 6458  df-f 6459  df-f1 6460  df-fo 6461  df-f1o 6462  df-fv 6463  df-isom 6464  df-riota 7261  df-ov 7307  df-oprab 7308  df-mpo 7309  df-of 7562  df-om 7742  df-1st 7860  df-2nd 7861  df-supp 8006  df-frecs 8125  df-wrecs 8156  df-recs 8230  df-rdg 8269  df-1o 8325  df-2o 8326  df-er 8526  df-map 8645  df-ixp 8714  df-en 8762  df-dom 8763  df-sdom 8764  df-fin 8765  df-fsupp 9170  df-fi 9211  df-sup 9242  df-inf 9243  df-oi 9310  df-card 9738  df-pnf 11054  df-mnf 11055  df-xr 11056  df-ltxr 11057  df-le 11058  df-sub 11250  df-neg 11251  df-div 11676  df-nn 12017  df-2 12079  df-3 12080  df-4 12081  df-5 12082  df-6 12083  df-7 12084  df-8 12085  df-9 12086  df-n0 12277  df-z 12363  df-dec 12481  df-uz 12626  df-q 12732  df-rp 12774  df-xneg 12891  df-xadd 12892  df-xmul 12893  df-ioo 13126  df-icc 13129  df-fz 13283  df-fzo 13426  df-seq 13765  df-exp 13826  df-hash 14088  df-cj 14852  df-re 14853  df-im 14854  df-sqrt 14988  df-abs 14989  df-struct 16890  df-sets 16907  df-slot 16925  df-ndx 16937  df-base 16955  df-ress 16984  df-plusg 17017  df-mulr 17018  df-starv 17019  df-sca 17020  df-vsca 17021  df-ip 17022  df-tset 17023  df-ple 17024  df-ds 17026  df-unif 17027  df-hom 17028  df-cco 17029  df-rest 17175  df-topn 17176  df-0g 17194  df-gsum 17195  df-topgen 17196  df-pt 17197  df-prds 17200  df-xrs 17255  df-qtop 17260  df-imas 17261  df-xps 17263  df-mre 17337  df-mrc 17338  df-acs 17340  df-mgm 18368  df-sgrp 18417  df-mnd 18428  df-submnd 18473  df-mulg 18743  df-cntz 18965  df-cmn 19430  df-psmet 20631  df-xmet 20632  df-met 20633  df-bl 20634  df-mopn 20635  df-cnfld 20640  df-top 22085  df-topon 22102  df-topsp 22124  df-bases 22138  df-cn 22420  df-cnp 22421  df-tx 22755  df-hmeo 22948  df-xms 23515  df-ms 23516  df-tms 23517  df-cncf 24083
This theorem is referenced by:  dya2iocnei  32291
  Copyright terms: Public domain W3C validator