Step | Hyp | Ref
| Expression |
1 | | limccnp2.j |
. . . . 5
⊢ 𝐽 = ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) |
2 | | limccnp2cntop.k |
. . . . . . . 8
⊢ 𝐾 = (MetOpen‘(abs ∘
− )) |
3 | 2 | cntoptopon 13130 |
. . . . . . 7
⊢ 𝐾 ∈
(TopOn‘ℂ) |
4 | | txtopon 12860 |
. . . . . . 7
⊢ ((𝐾 ∈ (TopOn‘ℂ)
∧ 𝐾 ∈
(TopOn‘ℂ)) → (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ ×
ℂ))) |
5 | 3, 3, 4 | mp2an 423 |
. . . . . 6
⊢ (𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ
× ℂ)) |
6 | | limccnp2.x |
. . . . . . 7
⊢ (𝜑 → 𝑋 ⊆ ℂ) |
7 | | limccnp2.y |
. . . . . . 7
⊢ (𝜑 → 𝑌 ⊆ ℂ) |
8 | | xpss12 4708 |
. . . . . . 7
⊢ ((𝑋 ⊆ ℂ ∧ 𝑌 ⊆ ℂ) → (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ)) |
9 | 6, 7, 8 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝑋 × 𝑌) ⊆ (ℂ ×
ℂ)) |
10 | | resttopon 12769 |
. . . . . 6
⊢ (((𝐾 ×t 𝐾) ∈ (TopOn‘(ℂ
× ℂ)) ∧ (𝑋
× 𝑌) ⊆ (ℂ
× ℂ)) → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ (TopOn‘(𝑋 × 𝑌))) |
11 | 5, 9, 10 | sylancr 411 |
. . . . 5
⊢ (𝜑 → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ (TopOn‘(𝑋 × 𝑌))) |
12 | 1, 11 | eqeltrid 2251 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ (TopOn‘(𝑋 × 𝑌))) |
13 | 3 | a1i 9 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
(TopOn‘ℂ)) |
14 | | limccnp2.h |
. . . 4
⊢ (𝜑 → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) |
15 | | cnpf2 12805 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘(𝑋 × 𝑌)) ∧ 𝐾 ∈ (TopOn‘ℂ) ∧ 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
16 | 12, 13, 14, 15 | syl3anc 1227 |
. . 3
⊢ (𝜑 → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
17 | 2 | cntoptop 13131 |
. . . . . . . . . . 11
⊢ 𝐾 ∈ Top |
18 | 17 | a1i 9 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ Top) |
19 | | txtop 12858 |
. . . . . . . . . . 11
⊢ ((𝐾 ∈ Top ∧ 𝐾 ∈ Top) → (𝐾 ×t 𝐾) ∈ Top) |
20 | 17, 18, 19 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 ×t 𝐾) ∈ Top) |
21 | | cnex 7871 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
22 | 21 | a1i 9 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈
V) |
23 | 22, 6 | ssexd 4119 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ V) |
24 | 22, 7 | ssexd 4119 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 ∈ V) |
25 | | xpexg 4715 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ V ∧ 𝑌 ∈ V) → (𝑋 × 𝑌) ∈ V) |
26 | 23, 24, 25 | syl2anc 409 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑋 × 𝑌) ∈ V) |
27 | | resttop 12768 |
. . . . . . . . . 10
⊢ (((𝐾 ×t 𝐾) ∈ Top ∧ (𝑋 × 𝑌) ∈ V) → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ Top) |
28 | 20, 26, 27 | syl2anc 409 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) ∈ Top) |
29 | 1, 28 | eqeltrid 2251 |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ Top) |
30 | | toptopon2 12615 |
. . . . . . . 8
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
31 | 29, 30 | sylib 121 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
32 | | cnprcl2k 12804 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐾 ∈ Top ∧
𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) → 〈𝐶, 𝐷〉 ∈ ∪
𝐽) |
33 | 31, 18, 14, 32 | syl3anc 1227 |
. . . . . 6
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ ∪
𝐽) |
34 | | toponuni 12611 |
. . . . . . 7
⊢ (𝐽 ∈ (TopOn‘(𝑋 × 𝑌)) → (𝑋 × 𝑌) = ∪ 𝐽) |
35 | 12, 34 | syl 14 |
. . . . . 6
⊢ (𝜑 → (𝑋 × 𝑌) = ∪ 𝐽) |
36 | 33, 35 | eleqtrrd 2244 |
. . . . 5
⊢ (𝜑 → 〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌)) |
37 | | opelxp 4631 |
. . . . 5
⊢
(〈𝐶, 𝐷〉 ∈ (𝑋 × 𝑌) ↔ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) |
38 | 36, 37 | sylib 121 |
. . . 4
⊢ (𝜑 → (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) |
39 | 38 | simpld 111 |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝑋) |
40 | 38 | simprd 113 |
. . 3
⊢ (𝜑 → 𝐷 ∈ 𝑌) |
41 | 16, 39, 40 | fovrnd 5980 |
. 2
⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ℂ) |
42 | | txrest 12874 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑋 ∈ V ∧ 𝑌 ∈ V)) → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) = ((𝐾 ↾t 𝑋) ×t (𝐾 ↾t 𝑌))) |
43 | 18, 18, 23, 24, 42 | syl22anc 1228 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐾 ×t 𝐾) ↾t (𝑋 × 𝑌)) = ((𝐾 ↾t 𝑋) ×t (𝐾 ↾t 𝑌))) |
44 | 1, 43 | syl5eq 2209 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐽 = ((𝐾 ↾t 𝑋) ×t (𝐾 ↾t 𝑌))) |
45 | | cnxmet 13129 |
. . . . . . . . . . . . 13
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
46 | | eqid 2164 |
. . . . . . . . . . . . . 14
⊢ ((abs
∘ − ) ↾ (𝑋 × 𝑋)) = ((abs ∘ − ) ↾ (𝑋 × 𝑋)) |
47 | | eqid 2164 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝑋 × 𝑋))) = (MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋))) |
48 | 46, 2, 47 | metrest 13104 |
. . . . . . . . . . . . 13
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → (𝐾 ↾t 𝑋) = (MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋)))) |
49 | 45, 6, 48 | sylancr 411 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾t 𝑋) = (MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋)))) |
50 | | eqid 2164 |
. . . . . . . . . . . . . 14
⊢ ((abs
∘ − ) ↾ (𝑌 × 𝑌)) = ((abs ∘ − ) ↾ (𝑌 × 𝑌)) |
51 | | eqid 2164 |
. . . . . . . . . . . . . 14
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌))) = (MetOpen‘((abs ∘ − )
↾ (𝑌 × 𝑌))) |
52 | 50, 2, 51 | metrest 13104 |
. . . . . . . . . . . . 13
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → (𝐾 ↾t 𝑌) = (MetOpen‘((abs ∘ − )
↾ (𝑌 × 𝑌)))) |
53 | 45, 7, 52 | sylancr 411 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐾 ↾t 𝑌) = (MetOpen‘((abs ∘ − )
↾ (𝑌 × 𝑌)))) |
54 | 49, 53 | oveq12d 5857 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐾 ↾t 𝑋) ×t (𝐾 ↾t 𝑌)) = ((MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋))) ×t
(MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌))))) |
55 | 44, 54 | eqtrd 2197 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 = ((MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋))) ×t
(MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌))))) |
56 | 55 | oveq1d 5854 |
. . . . . . . . 9
⊢ (𝜑 → (𝐽 CnP 𝐾) = (((MetOpen‘((abs ∘ − )
↾ (𝑋 × 𝑋))) ×t
(MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌)))) CnP 𝐾)) |
57 | 56 | fveq1d 5485 |
. . . . . . . 8
⊢ (𝜑 → ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉) = ((((MetOpen‘((abs ∘
− ) ↾ (𝑋
× 𝑋)))
×t (MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌)))) CnP 𝐾)‘〈𝐶, 𝐷〉)) |
58 | 14, 57 | eleqtrd 2243 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ∈ ((((MetOpen‘((abs ∘
− ) ↾ (𝑋
× 𝑋)))
×t (MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌)))) CnP 𝐾)‘〈𝐶, 𝐷〉)) |
59 | | xmetres2 12977 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑋 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑋
× 𝑋)) ∈
(∞Met‘𝑋)) |
60 | 45, 6, 59 | sylancr 411 |
. . . . . . . 8
⊢ (𝜑 → ((abs ∘ − )
↾ (𝑋 × 𝑋)) ∈
(∞Met‘𝑋)) |
61 | | xmetres2 12977 |
. . . . . . . . 9
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑌 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑌
× 𝑌)) ∈
(∞Met‘𝑌)) |
62 | 45, 7, 61 | sylancr 411 |
. . . . . . . 8
⊢ (𝜑 → ((abs ∘ − )
↾ (𝑌 × 𝑌)) ∈
(∞Met‘𝑌)) |
63 | 45 | a1i 9 |
. . . . . . . 8
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
64 | 47, 51, 2 | txmetcnp 13116 |
. . . . . . . 8
⊢ (((((abs
∘ − ) ↾ (𝑋 × 𝑋)) ∈ (∞Met‘𝑋) ∧ ((abs ∘ − )
↾ (𝑌 × 𝑌)) ∈
(∞Met‘𝑌) ∧
(abs ∘ − ) ∈ (∞Met‘ℂ)) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑌)) → (𝐻 ∈ ((((MetOpen‘((abs ∘
− ) ↾ (𝑋
× 𝑋)))
×t (MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌)))) CnP 𝐾)‘〈𝐶, 𝐷〉) ↔ (𝐻:(𝑋 × 𝑌)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑗 ∈
ℝ+ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)))) |
65 | 60, 62, 63, 38, 64 | syl31anc 1230 |
. . . . . . 7
⊢ (𝜑 → (𝐻 ∈ ((((MetOpen‘((abs ∘
− ) ↾ (𝑋
× 𝑋)))
×t (MetOpen‘((abs ∘ − ) ↾ (𝑌 × 𝑌)))) CnP 𝐾)‘〈𝐶, 𝐷〉) ↔ (𝐻:(𝑋 × 𝑌)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑗 ∈
ℝ+ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)))) |
66 | 58, 65 | mpbid 146 |
. . . . . 6
⊢ (𝜑 → (𝐻:(𝑋 × 𝑌)⟶ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑗 ∈
ℝ+ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) |
67 | 66 | simprd 113 |
. . . . 5
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑗 ∈ ℝ+
∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)) |
68 | 67 | r19.21bi 2552 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑗 ∈
ℝ+ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)) |
69 | | simpll 519 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) → 𝜑) |
70 | | simprl 521 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) → 𝑗 ∈ ℝ+) |
71 | | limccnp2.c |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) |
72 | | eqid 2164 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
73 | | limccnp2.r |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋) |
74 | 72, 73 | dmmptd 5315 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴) |
75 | | limcrcl 13225 |
. . . . . . . . . . . . 13
⊢ (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵) → ((𝑥 ∈ 𝐴 ↦ 𝑅):dom (𝑥 ∈ 𝐴 ↦ 𝑅)⟶ℂ ∧ dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
76 | 71, 75 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅):dom (𝑥 ∈ 𝐴 ↦ 𝑅)⟶ℂ ∧ dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ ∧ 𝐵 ∈ ℂ)) |
77 | 76 | simp2d 999 |
. . . . . . . . . . 11
⊢ (𝜑 → dom (𝑥 ∈ 𝐴 ↦ 𝑅) ⊆ ℂ) |
78 | 74, 77 | eqsstrrd 3177 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
79 | 76 | simp3d 1000 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) |
80 | 6 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑋 ⊆ ℂ) |
81 | 80, 73 | sseldd 3141 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
82 | 78, 79, 81 | limcmpted 13230 |
. . . . . . . . 9
⊢ (𝜑 → (𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵) ↔ (𝐶 ∈ ℂ ∧ ∀𝑗 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)))) |
83 | 71, 82 | mpbid 146 |
. . . . . . . 8
⊢ (𝜑 → (𝐶 ∈ ℂ ∧ ∀𝑗 ∈ ℝ+
∃𝑓 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) |
84 | 83 | simprd 113 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ ℝ+ ∃𝑓 ∈ ℝ+
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)) |
85 | 84 | r19.21bi 2552 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℝ+) →
∃𝑓 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)) |
86 | 69, 70, 85 | syl2anc 409 |
. . . . 5
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) → ∃𝑓 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)) |
87 | 69 | adantr 274 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) → 𝜑) |
88 | | simplrl 525 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) → 𝑗 ∈ ℝ+) |
89 | | limccnp2.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) |
90 | 7 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ⊆ ℂ) |
91 | | limccnp2.s |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌) |
92 | 90, 91 | sseldd 3141 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ ℂ) |
93 | 78, 79, 92 | limcmpted 13230 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵) ↔ (𝐷 ∈ ℂ ∧ ∀𝑗 ∈ ℝ+
∃𝑔 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)))) |
94 | 89, 93 | mpbid 146 |
. . . . . . . . 9
⊢ (𝜑 → (𝐷 ∈ ℂ ∧ ∀𝑗 ∈ ℝ+
∃𝑔 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) |
95 | 94 | simprd 113 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ ℝ+ ∃𝑔 ∈ ℝ+
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)) |
96 | 95 | r19.21bi 2552 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℝ+) →
∃𝑔 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)) |
97 | 87, 88, 96 | syl2anc 409 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) → ∃𝑔 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)) |
98 | | simp-5l 533 |
. . . . . . . 8
⊢
((((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) ∧ 𝑥 ∈ 𝐴) → 𝜑) |
99 | 98, 73 | sylancom 417 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ 𝑋) |
100 | 98, 91 | sylancom 417 |
. . . . . . 7
⊢
((((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) ∧ 𝑥 ∈ 𝐴) → 𝑆 ∈ 𝑌) |
101 | 6 | ad4antr 486 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑋 ⊆ ℂ) |
102 | 7 | ad4antr 486 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑌 ⊆ ℂ) |
103 | 71 | ad4antr 486 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝐶 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑅) limℂ 𝐵)) |
104 | 89 | ad4antr 486 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝐷 ∈ ((𝑥 ∈ 𝐴 ↦ 𝑆) limℂ 𝐵)) |
105 | 14 | ad4antr 486 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝐻 ∈ ((𝐽 CnP 𝐾)‘〈𝐶, 𝐷〉)) |
106 | | nfv 1515 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) |
107 | | nfv 1515 |
. . . . . . . . . 10
⊢
Ⅎ𝑥 𝑓 ∈
ℝ+ |
108 | | nfra1 2495 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗) |
109 | 107, 108 | nfan 1552 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑓 ∈ ℝ+
∧ ∀𝑥 ∈
𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)) |
110 | 106, 109 | nfan 1552 |
. . . . . . . 8
⊢
Ⅎ𝑥(((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) |
111 | | nfv 1515 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑔 ∈
ℝ+ |
112 | | nfra1 2495 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗) |
113 | 111, 112 | nfan 1552 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑔 ∈ ℝ+
∧ ∀𝑥 ∈
𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)) |
114 | 110, 113 | nfan 1552 |
. . . . . . 7
⊢
Ⅎ𝑥((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) |
115 | | simp-4r 532 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑒 ∈ ℝ+) |
116 | 70 | ad2antrr 480 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑗 ∈ ℝ+) |
117 | | simprr 522 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) → ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)) |
118 | 117 | ad2antrr 480 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒)) |
119 | | simplrl 525 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑓 ∈ ℝ+) |
120 | | simplrr 526 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗)) |
121 | | simprl 521 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → 𝑔 ∈ ℝ+) |
122 | | simprr 522 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗)) |
123 | 99, 100, 101, 102, 2, 1, 103, 104, 105, 114, 115, 116, 118, 119, 120, 121, 122 | limccnp2lem 13243 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑒 ∈ ℝ+)
∧ (𝑗 ∈
ℝ+ ∧ ∀𝑟 ∈ 𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) ∧ (𝑔 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑔) → (abs‘(𝑆 − 𝐷)) < 𝑗))) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)) |
124 | 97, 123 | rexlimddv 2586 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) ∧ (𝑓 ∈ ℝ+ ∧
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑓) → (abs‘(𝑅 − 𝐶)) < 𝑗))) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)) |
125 | 86, 124 | rexlimddv 2586 |
. . . 4
⊢ (((𝜑 ∧ 𝑒 ∈ ℝ+) ∧ (𝑗 ∈ ℝ+
∧ ∀𝑟 ∈
𝑋 ∀𝑠 ∈ 𝑌 (((𝐶((abs ∘ − ) ↾ (𝑋 × 𝑋))𝑟) < 𝑗 ∧ (𝐷((abs ∘ − ) ↾ (𝑌 × 𝑌))𝑠) < 𝑗) → ((𝐶𝐻𝐷)(abs ∘ − )(𝑟𝐻𝑠)) < 𝑒))) → ∃𝑑 ∈ ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)) |
126 | 68, 125 | rexlimddv 2586 |
. . 3
⊢ ((𝜑 ∧ 𝑒 ∈ ℝ+) →
∃𝑑 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)) |
127 | 126 | ralrimiva 2537 |
. 2
⊢ (𝜑 → ∀𝑒 ∈ ℝ+ ∃𝑑 ∈ ℝ+
∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)) |
128 | 16 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐻:(𝑋 × 𝑌)⟶ℂ) |
129 | 128, 73, 91 | fovrnd 5980 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅𝐻𝑆) ∈ ℂ) |
130 | 78, 79, 129 | limcmpted 13230 |
. 2
⊢ (𝜑 → ((𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵) ↔ ((𝐶𝐻𝐷) ∈ ℂ ∧ ∀𝑒 ∈ ℝ+
∃𝑑 ∈
ℝ+ ∀𝑥 ∈ 𝐴 ((𝑥 # 𝐵 ∧ (abs‘(𝑥 − 𝐵)) < 𝑑) → (abs‘((𝑅𝐻𝑆) − (𝐶𝐻𝐷))) < 𝑒)))) |
131 | 41, 127, 130 | mpbir2and 933 |
1
⊢ (𝜑 → (𝐶𝐻𝐷) ∈ ((𝑥 ∈ 𝐴 ↦ (𝑅𝐻𝑆)) limℂ 𝐵)) |