Step | Hyp | Ref
| Expression |
1 | | xrlimcnp.r |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
2 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
3 | 1, 2 | fmptd 6385 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
4 | 3 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
5 | | ssun2 3777 |
. . . . . . . . . 10
⊢
{+∞} ⊆ (𝐵 ∪ {+∞}) |
6 | | pnfex 10093 |
. . . . . . . . . . 11
⊢ +∞
∈ V |
7 | 6 | snid 4208 |
. . . . . . . . . 10
⊢ +∞
∈ {+∞} |
8 | 5, 7 | sselii 3600 |
. . . . . . . . 9
⊢ +∞
∈ (𝐵 ∪
{+∞}) |
9 | | xrlimcnp.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞})) |
10 | 8, 9 | syl5eleqr 2708 |
. . . . . . . 8
⊢ (𝜑 → +∞ ∈ 𝐴) |
11 | 1 | ralrimiva 2966 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
12 | | xrlimcnp.c |
. . . . . . . . . . 11
⊢ (𝑥 = +∞ → 𝑅 = 𝐶) |
13 | 12 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈
ℂ)) |
14 | 13 | rspcv 3305 |
. . . . . . . . 9
⊢ (+∞
∈ 𝐴 →
(∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → 𝐶 ∈ ℂ)) |
15 | 10, 11, 14 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
16 | 12, 2 | fvmptg 6280 |
. . . . . . . 8
⊢
((+∞ ∈ 𝐴
∧ 𝐶 ∈ ℂ)
→ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
17 | 10, 15, 16 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
18 | 17 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
19 | 18 | eleq1d 2686 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦)) |
20 | | cnxmet 22576 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
21 | | xrlimcnp.j |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘ℂfld) |
22 | 21 | cnfldtopn 22585 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
23 | 22 | mopni2 22298 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦) |
24 | 20, 23 | mp3an1 1411 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦) |
25 | | ssun1 3776 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ (𝐵 ∪ {+∞}) |
26 | 25, 9 | syl5sseqr 3654 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
27 | | ssralv 3666 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)) |
28 | 26, 11, 27 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
29 | 28 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
30 | | simprl 794 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+) |
31 | | simplr 792 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) |
32 | 29, 30, 31 | rlimi 14244 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
33 | | letop 21010 |
. . . . . . . . . . . . . . 15
⊢
(ordTop‘ ≤ ) ∈ Top |
34 | 33 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (ordTop‘ ≤ ) ∈
Top) |
35 | | xrlimcnp.b |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
36 | | ressxr 10083 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
⊆ ℝ* |
37 | 35, 36 | syl6ss 3615 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆
ℝ*) |
38 | | pnfxr 10092 |
. . . . . . . . . . . . . . . . . . . 20
⊢ +∞
∈ ℝ* |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → +∞ ∈
ℝ*) |
40 | 39 | snssd 4340 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {+∞} ⊆
ℝ*) |
41 | 37, 40 | unssd 3789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 ∪ {+∞}) ⊆
ℝ*) |
42 | 9, 41 | eqsstrd 3639 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
43 | | xrex 11829 |
. . . . . . . . . . . . . . . . 17
⊢
ℝ* ∈ V |
44 | 43 | ssex 4802 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ ℝ*
→ 𝐴 ∈
V) |
45 | 42, 44 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ V) |
46 | 45 | ad2antrr 762 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 ∈ V) |
47 | | iocpnfordt 21019 |
. . . . . . . . . . . . . . 15
⊢ (𝑘(,]+∞) ∈
(ordTop‘ ≤ ) |
48 | 47 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤
)) |
49 | | elrestr 16089 |
. . . . . . . . . . . . . 14
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
→ ((𝑘(,]+∞)
∩ 𝐴) ∈
((ordTop‘ ≤ ) ↾t 𝐴)) |
50 | 34, 46, 48, 49 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ )
↾t 𝐴)) |
51 | | xrlimcnp.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = ((ordTop‘ ≤ )
↾t 𝐴) |
52 | 50, 51 | syl6eleqr 2712 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾) |
53 | | simprl 794 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ) |
54 | 53 | rexrd 10089 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*) |
55 | 38 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈
ℝ*) |
56 | | ltpnf 11954 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℝ → 𝑘 < +∞) |
57 | 53, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 < +∞) |
58 | | ubioc1 12227 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞)) |
59 | 54, 55, 57, 58 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞)) |
60 | 10 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ 𝐴) |
61 | 59, 60 | elind 3798 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)) |
62 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
63 | 62 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ*) |
64 | | elioc1 12217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
65 | 63, 38, 64 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
66 | | simp2 1062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞) → 𝑘 < 𝑥) |
67 | 65, 66 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥)) |
68 | 35 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ) |
69 | 68 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ) |
70 | | ltle 10126 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥)) |
71 | 62, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥)) |
72 | 67, 71 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 ≤ 𝑥)) |
73 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
74 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+) |
75 | 74 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ+) |
76 | | rpxr 11840 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ*) |
78 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
79 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
80 | 79 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ) |
81 | | elbl3 22197 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
82 | 73, 77, 78, 80, 81 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
83 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (abs
∘ − ) = (abs ∘ − ) |
84 | 83 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
85 | 80, 78, 84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
86 | 85 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
87 | 82, 86 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
88 | 87 | biimprd 238 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((abs‘(𝑅 − 𝐶)) < 𝑟 → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
89 | 72, 88 | imim12d 81 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
90 | 89 | ralimdva 2962 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
91 | 90 | impr 649 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
92 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
93 | 15 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ ℂ) |
94 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+) |
95 | | blcntr 22218 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
96 | 92, 93, 94, 95 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
97 | 96 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
98 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞))) |
99 | 12 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
100 | 98, 99 | imbi12d 334 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
101 | 6, 100 | ralsn 4222 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
{+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
102 | 97, 101 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
103 | | ralunb 3794 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
(𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
104 | 91, 102, 103 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
105 | 9 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞})) |
106 | 105 | raleqdv 3144 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
107 | 104, 106 | mpbird 247 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
108 | | ss2rab 3678 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
109 | 107, 108 | sylibr 224 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}) |
110 | | incom 3805 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞)) |
111 | | dfin5 3582 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ (𝑘(,]+∞)) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} |
112 | 110, 111 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘(,]+∞) ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} |
113 | 2 | mptpreima 5628 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} |
114 | 109, 112,
113 | 3sstr4g 3646 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))) |
115 | | funmpt 5926 |
. . . . . . . . . . . . . . 15
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝑅) |
116 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴 |
117 | 3 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
118 | | fdm 6051 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴) |
120 | 116, 119 | syl5sseqr 3654 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) |
121 | | funimass3 6333 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
(𝑥 ∈ 𝐴 ↦ 𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
122 | 115, 120,
121 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
123 | 114, 122 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) |
124 | | simplrr 801 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦) |
125 | 123, 124 | sstrd 3613 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦) |
126 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))) |
127 | | imaeq2 5462 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴))) |
128 | 127 | sseq1d 3632 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) |
129 | 126, 128 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))) |
130 | 129 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
131 | 52, 61, 125, 130 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
132 | 131 | rexlimdvaa 3032 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
133 | 132 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
134 | 32, 133 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
135 | 134 | rexlimdvaa 3032 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑟) ⊆ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
136 | 24, 135 | syl5 34 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
137 | 136 | expdimp 453 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (𝐶 ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
138 | 19, 137 | sylbid 230 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
139 | 138 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
140 | | letopon 21009 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
141 | | resttopon 20965 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
𝐴 ⊆
ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
142 | 140, 42, 141 | sylancr 695 |
. . . . . 6
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴)
∈ (TopOn‘𝐴)) |
143 | 51, 142 | syl5eqel 2705 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐴)) |
144 | 21 | cnfldtopon 22586 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
145 | 144 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈
(TopOn‘ℂ)) |
146 | | iscnp 21041 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞
∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
147 | 143, 145,
10, 146 | syl3anc 1326 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
148 | 147 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
149 | 4, 139, 148 | mpbir2and 957 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) |
150 | | simplr 792 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) |
151 | 20 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
152 | 15 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈
ℂ) |
153 | 76 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
154 | 22 | blopn 22305 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑟) ∈ 𝐽) |
155 | 151, 152,
153, 154 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑟) ∈ 𝐽) |
156 | 17 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
157 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
158 | 151, 152,
157, 95 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
159 | 156, 158 | eqeltrd 2701 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
160 | | cnpimaex 21060 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
161 | 150, 155,
159, 160 | syl3anc 1326 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
162 | | vex 3203 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
163 | 162 | inex1 4799 |
. . . . . . . 8
⊢ (𝑤 ∩ 𝐴) ∈ V |
164 | 163 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
→ (𝑤 ∩ 𝐴) ∈ V) |
165 | 51 | eleq2i 2693 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)) |
166 | 45 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V) |
167 | | elrest 16088 |
. . . . . . . . 9
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)
↔ ∃𝑤 ∈
(ordTop‘ ≤ )𝑧 =
(𝑤 ∩ 𝐴))) |
168 | 33, 166, 167 | sylancr 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)
↔ ∃𝑤 ∈
(ordTop‘ ≤ )𝑧 =
(𝑤 ∩ 𝐴))) |
169 | 165, 168 | syl5bb 272 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ 𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴))) |
170 | | eleq2 2690 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤 ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤 ∩ 𝐴))) |
171 | | imaeq2 5462 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴))) |
172 | 171 | sseq1d 3632 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤 ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
173 | 170, 172 | anbi12d 747 |
. . . . . . . 8
⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
174 | 173 | adantl 482 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤 ∩ 𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
175 | 164, 169,
174 | rexxfr2d 4883 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
(∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤
)(+∞ ∈ (𝑤 ∩
𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
176 | 161, 175 | mpbid 222 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
177 | | inss1 3833 |
. . . . . . . . . . . 12
⊢ (𝑤 ∩ 𝐴) ⊆ 𝑤 |
178 | 177 | sseli 3599 |
. . . . . . . . . . 11
⊢ (+∞
∈ (𝑤 ∩ 𝐴) → +∞ ∈ 𝑤) |
179 | | pnfnei 21024 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝑤)
→ ∃𝑘 ∈
ℝ (𝑘(,]+∞)
⊆ 𝑤) |
180 | 178, 179 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ (𝑤
∩ 𝐴)) →
∃𝑘 ∈ ℝ
(𝑘(,]+∞) ⊆
𝑤) |
181 | | df-ima 5127 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) |
182 | | inss2 3834 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∩ 𝐴) ⊆ 𝐴 |
183 | | resmpt 5449 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)) |
184 | 182, 183 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
185 | 184 | rneqi 5352 |
. . . . . . . . . . . . . . . 16
⊢ ran
((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
186 | 181, 185 | eqtri 2644 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
187 | 186 | sseq1i 3629 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) |
188 | | dfss3 3592 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
189 | 187, 188 | bitri 264 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
190 | 11 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
191 | | ssralv 3666 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ)) |
192 | 182, 190,
191 | mpsyl 68 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ) |
193 | | eqid 2622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
194 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
195 | 193, 194 | ralrnmpt 6368 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
(𝑤 ∩ 𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
196 | 192, 195 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑧 ∈ ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
197 | 196 | biimpd 219 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑧 ∈ ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
198 | 189, 197 | syl5bi 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
199 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤) |
200 | 37 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐵 ⊆
ℝ*) |
201 | | simprl 794 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐵) |
202 | 200, 201 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ ℝ*) |
203 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 < 𝑥) |
204 | | pnfge 11964 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ ℝ*
→ 𝑥 ≤
+∞) |
205 | 202, 204 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ≤ +∞) |
206 | | simplrl 800 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ) |
207 | 206 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ*) |
208 | 207, 38, 64 | sylancl 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
209 | 202, 203,
205, 208 | mpbir3and 1245 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞)) |
210 | 199, 209 | sseldd 3604 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝑤) |
211 | 26 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵 ⊆ 𝐴) |
212 | 211 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
213 | 212 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐴) |
214 | 210, 213 | elind 3798 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑤 ∩ 𝐴)) |
215 | 214 | ex 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑥 ∈ (𝑤 ∩ 𝐴))) |
216 | 215 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
217 | 20 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
218 | 76 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
219 | 218 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑟 ∈ ℝ*) |
220 | 15 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐶 ∈ ℂ) |
221 | 28 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
222 | 221 | r19.21bi 2932 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ) |
223 | 222 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑅 ∈ ℂ) |
224 | 217, 219,
220, 223, 81 | syl22anc 1327 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
225 | 223, 220,
84 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
226 | 225 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
227 | 224, 226 | bitrd 268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
228 | 227 | pm5.74da 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
229 | 216, 228 | sylibd 229 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
230 | 229 | exp4a 633 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥 ∈ 𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
231 | 230 | ralimdv2 2961 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
232 | 231 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
233 | 232 | an32s 846 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
234 | 233 | expr 643 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
235 | 234 | reximdva 3017 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
236 | 235 | ex 450 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
237 | 198, 236 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
238 | 237 | com23 86 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑘 ∈ ℝ
(𝑘(,]+∞) ⊆
𝑤 → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
239 | 180, 238 | syl5 34 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ (𝑤
∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
240 | 239 | impl 650 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
∧ +∞ ∈ (𝑤
∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
241 | 240 | expimpd 629 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
→ ((+∞ ∈ (𝑤
∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
242 | 241 | rexlimdva 3031 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
243 | 242 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
244 | 176, 243 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
245 | 244 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
246 | 28, 35, 15 | rlim2lt 14228 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
247 | 246 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
248 | 245, 247 | mpbird 247 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) |
249 | 149, 248 | impbida 877 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))) |