Step | Hyp | Ref
| Expression |
1 | | xrlimcnp.r |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
2 | 1 | fmpttd 6649 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
3 | 2 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
4 | | eqid 2777 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
5 | | xrlimcnp.c |
. . . . . . . 8
⊢ (𝑥 = +∞ → 𝑅 = 𝐶) |
6 | | ssun2 3999 |
. . . . . . . . . 10
⊢
{+∞} ⊆ (𝐵 ∪ {+∞}) |
7 | | pnfex 10429 |
. . . . . . . . . . 11
⊢ +∞
∈ V |
8 | 7 | snid 4429 |
. . . . . . . . . 10
⊢ +∞
∈ {+∞} |
9 | 6, 8 | sselii 3817 |
. . . . . . . . 9
⊢ +∞
∈ (𝐵 ∪
{+∞}) |
10 | | xrlimcnp.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 = (𝐵 ∪ {+∞})) |
11 | 9, 10 | syl5eleqr 2865 |
. . . . . . . 8
⊢ (𝜑 → +∞ ∈ 𝐴) |
12 | 5 | eleq1d 2843 |
. . . . . . . . 9
⊢ (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈
ℂ)) |
13 | 1 | ralrimiva 3147 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
14 | 12, 13, 11 | rspcdva 3516 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
15 | 4, 5, 11, 14 | fvmptd3 6564 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
16 | 15 | ad2antrr 716 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
17 | 16 | eleq1d 2843 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦)) |
18 | | cnxmet 22984 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
19 | | xrlimcnp.j |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘ℂfld) |
20 | 19 | cnfldtopn 22993 |
. . . . . . . . 9
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
21 | 20 | mopni2 22706 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦) |
22 | 18, 21 | mp3an1 1521 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦) |
23 | | ssun1 3998 |
. . . . . . . . . . . . 13
⊢ 𝐵 ⊆ (𝐵 ∪ {+∞}) |
24 | 23, 10 | syl5sseqr 3872 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
25 | | ssralv 3884 |
. . . . . . . . . . . 12
⊢ (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ)) |
26 | 24, 13, 25 | sylc 65 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
27 | 26 | ad2antrr 716 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
28 | | simprl 761 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+) |
29 | | simplr 759 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) |
30 | 27, 28, 29 | rlimi 14652 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
31 | | letop 21418 |
. . . . . . . . . . . . . . 15
⊢
(ordTop‘ ≤ ) ∈ Top |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (ordTop‘ ≤ ) ∈
Top) |
33 | | xrlimcnp.b |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
34 | | ressxr 10420 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℝ
⊆ ℝ* |
35 | 33, 34 | syl6ss 3832 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ⊆
ℝ*) |
36 | | pnfxr 10430 |
. . . . . . . . . . . . . . . . . . . 20
⊢ +∞
∈ ℝ* |
37 | 36 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → +∞ ∈
ℝ*) |
38 | 37 | snssd 4571 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → {+∞} ⊆
ℝ*) |
39 | 35, 38 | unssd 4011 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐵 ∪ {+∞}) ⊆
ℝ*) |
40 | 10, 39 | eqsstrd 3857 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ⊆
ℝ*) |
41 | | xrex 12134 |
. . . . . . . . . . . . . . . . 17
⊢
ℝ* ∈ V |
42 | 41 | ssex 5039 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ ℝ*
→ 𝐴 ∈
V) |
43 | 40, 42 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ V) |
44 | 43 | ad2antrr 716 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 ∈ V) |
45 | | iocpnfordt 21427 |
. . . . . . . . . . . . . . 15
⊢ (𝑘(,]+∞) ∈
(ordTop‘ ≤ ) |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤
)) |
47 | | elrestr 16475 |
. . . . . . . . . . . . . 14
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
→ ((𝑘(,]+∞)
∩ 𝐴) ∈
((ordTop‘ ≤ ) ↾t 𝐴)) |
48 | 32, 44, 46, 47 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ )
↾t 𝐴)) |
49 | | xrlimcnp.k |
. . . . . . . . . . . . 13
⊢ 𝐾 = ((ordTop‘ ≤ )
↾t 𝐴) |
50 | 48, 49 | syl6eleqr 2869 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾) |
51 | | simprl 761 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ) |
52 | 51 | rexrd 10426 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*) |
53 | 36 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈
ℝ*) |
54 | | ltpnf 12265 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ℝ → 𝑘 < +∞) |
55 | 51, 54 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑘 < +∞) |
56 | | ubioc1 12539 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℝ*
∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞)) |
57 | 52, 53, 55, 56 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞)) |
58 | 11 | ad2antrr 716 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ 𝐴) |
59 | 57, 58 | elind 4020 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)) |
60 | | simplr 759 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ) |
61 | 60 | rexrd 10426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑘 ∈ ℝ*) |
62 | | elioc1 12529 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑘 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
63 | 61, 36, 62 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
64 | | simp2 1128 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℝ*
∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞) → 𝑘 < 𝑥) |
65 | 63, 64 | syl6bi 245 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥)) |
66 | 33 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ) |
67 | 66 | sselda 3820 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ ℝ) |
68 | | ltle 10465 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥)) |
69 | 60, 67, 68 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑘 < 𝑥 → 𝑘 ≤ 𝑥)) |
70 | 65, 69 | syld 47 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 ≤ 𝑥)) |
71 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
72 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+) |
73 | 72 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ+) |
74 | | rpxr 12148 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 ∈ ℝ+
→ 𝑟 ∈
ℝ*) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑟 ∈ ℝ*) |
76 | 14 | ad3antrrr 720 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝐶 ∈ ℂ) |
77 | 26 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
78 | 77 | r19.21bi 3113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ) |
79 | | elbl3 22605 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
80 | 71, 75, 76, 78, 79 | syl22anc 829 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
81 | | eqid 2777 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (abs
∘ − ) = (abs ∘ − ) |
82 | 81 | cnmetdval 22982 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
83 | 78, 76, 82 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
84 | 83 | breq1d 4896 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
85 | 80, 84 | bitrd 271 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
86 | 85 | biimprd 240 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((abs‘(𝑅 − 𝐶)) < 𝑟 → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
87 | 70, 86 | imim12d 81 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥 ∈ 𝐵) → ((𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
88 | 87 | ralimdva 3143 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
89 | 88 | impr 448 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
90 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
91 | 14 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ ℂ) |
92 | | simplrl 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+) |
93 | | blcntr 22626 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
94 | 90, 91, 92, 93 | syl3anc 1439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
95 | 94 | a1d 25 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
96 | | eleq1 2846 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞))) |
97 | 5 | eleq1d 2843 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
98 | 96, 97 | imbi12d 336 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
99 | 7, 98 | ralsn 4449 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
{+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
100 | 95, 99 | sylibr 226 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
101 | | ralunb 4016 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑥 ∈
(𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥 ∈ 𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
102 | 89, 100, 101 | sylanbrc 578 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
103 | 10 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞})) |
104 | 103 | raleqdv 3339 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
105 | 102, 104 | mpbird 249 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
106 | | ss2rab 3898 |
. . . . . . . . . . . . . . . 16
⊢ ({𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥 ∈ 𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
107 | 105, 106 | sylibr 226 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}) |
108 | | incom 4027 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞)) |
109 | | dfin5 3799 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∩ (𝑘(,]+∞)) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} |
110 | 108, 109 | eqtri 2801 |
. . . . . . . . . . . . . . 15
⊢ ((𝑘(,]+∞) ∩ 𝐴) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ (𝑘(,]+∞)} |
111 | 4 | mptpreima 5882 |
. . . . . . . . . . . . . . 15
⊢ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥 ∈ 𝐴 ∣ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} |
112 | 107, 110,
111 | 3sstr4g 3864 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))) |
113 | | funmpt 6173 |
. . . . . . . . . . . . . . 15
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝑅) |
114 | | inss2 4053 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴 |
115 | 2 | ad2antrr 716 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
116 | 115 | fdmd 6300 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → dom (𝑥 ∈ 𝐴 ↦ 𝑅) = 𝐴) |
117 | 114, 116 | syl5sseqr 3872 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) |
118 | | funimass3 6596 |
. . . . . . . . . . . . . . 15
⊢ ((Fun
(𝑥 ∈ 𝐴 ↦ 𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥 ∈ 𝐴 ↦ 𝑅)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
119 | 113, 117,
118 | sylancr 581 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ (◡(𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
120 | 112, 119 | mpbird 249 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) |
121 | | simplrr 768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦) |
122 | 120, 121 | sstrd 3830 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦) |
123 | | eleq2 2847 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))) |
124 | | imaeq2 5716 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴))) |
125 | 124 | sseq1d 3850 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) |
126 | 123, 125 | anbi12d 624 |
. . . . . . . . . . . . 13
⊢ (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))) |
127 | 126 | rspcev 3510 |
. . . . . . . . . . . 12
⊢ ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
128 | 50, 59, 122, 127 | syl12anc 827 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
129 | 128 | rexlimdvaa 3213 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
130 | 129 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 ≤ 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
131 | 30, 130 | mpd 15 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ −
))𝑟) ⊆ 𝑦)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦)) |
132 | 131 | rexlimdvaa 3213 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+
(𝐶(ball‘(abs ∘
− ))𝑟) ⊆ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
133 | 22, 132 | syl5 34 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
134 | 133 | expdimp 446 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (𝐶 ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
135 | 17, 134 | sylbid 232 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
136 | 135 | ralrimiva 3147 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))) |
137 | | letopon 21417 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
138 | | resttopon 21373 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
𝐴 ⊆
ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴)) |
139 | 137, 40, 138 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → ((ordTop‘ ≤ )
↾t 𝐴)
∈ (TopOn‘𝐴)) |
140 | 49, 139 | syl5eqel 2862 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐴)) |
141 | 19 | cnfldtopon 22994 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘ℂ) |
142 | 141 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈
(TopOn‘ℂ)) |
143 | | iscnp 21449 |
. . . . 5
⊢ ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞
∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
144 | 140, 142,
11, 143 | syl3anc 1439 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
145 | 144 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑦 ∈ 𝐽 (((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ 𝑦 → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ 𝑦))))) |
146 | 3, 136, 145 | mpbir2and 703 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) |
147 | | simplr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) |
148 | 18 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (abs
∘ − ) ∈ (∞Met‘ℂ)) |
149 | 14 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈
ℂ) |
150 | 74 | adantl 475 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
151 | 20 | blopn 22713 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ −
))𝑟) ∈ 𝐽) |
152 | 148, 149,
150, 151 | syl3anc 1439 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ −
))𝑟) ∈ 𝐽) |
153 | 15 | ad2antrr 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) = 𝐶) |
154 | | simpr 479 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ+) |
155 | 148, 149,
154, 93 | syl3anc 1439 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
156 | 153, 155 | eqeltrd 2858 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
157 | | cnpimaex 21468 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
158 | 147, 152,
156, 157 | syl3anc 1439 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
159 | | vex 3400 |
. . . . . . . . 9
⊢ 𝑤 ∈ V |
160 | 159 | inex1 5036 |
. . . . . . . 8
⊢ (𝑤 ∩ 𝐴) ∈ V |
161 | 160 | a1i 11 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
→ (𝑤 ∩ 𝐴) ∈ V) |
162 | 49 | eleq2i 2850 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)) |
163 | 43 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V) |
164 | | elrest 16474 |
. . . . . . . . 9
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)
↔ ∃𝑤 ∈
(ordTop‘ ≤ )𝑧 =
(𝑤 ∩ 𝐴))) |
165 | 31, 163, 164 | sylancr 581 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ )
↾t 𝐴)
↔ ∃𝑤 ∈
(ordTop‘ ≤ )𝑧 =
(𝑤 ∩ 𝐴))) |
166 | 162, 165 | syl5bb 275 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ 𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤 ∩ 𝐴))) |
167 | | eleq2 2847 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤 ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤 ∩ 𝐴))) |
168 | | imaeq2 5716 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) = ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴))) |
169 | 168 | sseq1d 3850 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤 ∩ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
170 | 167, 169 | anbi12d 624 |
. . . . . . . 8
⊢ (𝑧 = (𝑤 ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
171 | 170 | adantl 475 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤 ∩ 𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈
(𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
172 | 161, 166,
171 | rexxfr2d 5123 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
(∃𝑧 ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤
)(+∞ ∈ (𝑤 ∩
𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
173 | 158, 172 | mpbid 224 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))) |
174 | | inss1 4052 |
. . . . . . . . . . . 12
⊢ (𝑤 ∩ 𝐴) ⊆ 𝑤 |
175 | 174 | sseli 3816 |
. . . . . . . . . . 11
⊢ (+∞
∈ (𝑤 ∩ 𝐴) → +∞ ∈ 𝑤) |
176 | | pnfnei 21432 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝑤)
→ ∃𝑘 ∈
ℝ (𝑘(,]+∞)
⊆ 𝑤) |
177 | 175, 176 | sylan2 586 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ (𝑤
∩ 𝐴)) →
∃𝑘 ∈ ℝ
(𝑘(,]+∞) ⊆
𝑤) |
178 | | df-ima 5368 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) |
179 | | inss2 4053 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∩ 𝐴) ⊆ 𝐴 |
180 | | resmpt 5699 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)) |
181 | 179, 180 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
182 | 181 | rneqi 5597 |
. . . . . . . . . . . . . . . 16
⊢ ran
((𝑥 ∈ 𝐴 ↦ 𝑅) ↾ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
183 | 178, 182 | eqtri 2801 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) = ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
184 | 183 | sseq1i 3847 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) |
185 | | dfss3 3809 |
. . . . . . . . . . . . . 14
⊢ (ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
186 | 184, 185 | bitri 267 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) |
187 | 13 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
188 | | ssralv 3884 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∩ 𝐴) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ)) |
189 | 179, 187,
188 | mpsyl 68 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ ℂ) |
190 | | eqid 2777 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅) |
191 | | eleq1 2846 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
192 | 190, 191 | ralrnmpt 6632 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑥 ∈
(𝑤 ∩ 𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
193 | 189, 192 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑧 ∈ ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
194 | 193 | biimpd 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑧 ∈ ran
(𝑥 ∈ (𝑤 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
195 | 186, 194 | syl5bi 234 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))) |
196 | | simplrr 768 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤) |
197 | 35 | ad3antrrr 720 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐵 ⊆
ℝ*) |
198 | | simprl 761 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐵) |
199 | 197, 198 | sseldd 3821 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ ℝ*) |
200 | | simprr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 < 𝑥) |
201 | | pnfge 12275 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ ℝ*
→ 𝑥 ≤
+∞) |
202 | 199, 201 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ≤ +∞) |
203 | | simplrl 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ) |
204 | 203 | rexrd 10426 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑘 ∈ ℝ*) |
205 | 204, 36, 62 | sylancl 580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞))) |
206 | 199, 200,
202, 205 | mpbir3and 1399 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞)) |
207 | 196, 206 | sseldd 3821 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝑤) |
208 | 24 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵 ⊆ 𝐴) |
209 | 208 | sselda 3820 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
210 | 209 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ 𝐴) |
211 | 207, 210 | elind 4020 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑥 ∈ (𝑤 ∩ 𝐴)) |
212 | 211 | ex 403 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑥 ∈ (𝑤 ∩ 𝐴))) |
213 | 212 | imim1d 82 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))) |
214 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
215 | 74 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈
ℝ*) |
216 | 215 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑟 ∈ ℝ*) |
217 | 14 | ad3antrrr 720 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝐶 ∈ ℂ) |
218 | 26 | ad2antrr 716 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 𝑅 ∈ ℂ) |
219 | 218 | r19.21bi 3113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥 ∈ 𝐵) → 𝑅 ∈ ℂ) |
220 | 219 | adantrr 707 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → 𝑅 ∈ ℂ) |
221 | 214, 216,
217, 220, 79 | syl22anc 829 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟)) |
222 | 220, 217,
82 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
223 | 222 | breq1d 4896 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
224 | 221, 223 | bitrd 271 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅 − 𝐶)) < 𝑟)) |
225 | 224 | pm5.74da 794 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
226 | 213, 225 | sylibd 231 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥) → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
227 | 226 | exp4a 424 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤 ∩ 𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥 ∈ 𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
228 | 227 | ralimdv2 3142 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
229 | 228 | imp 397 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
230 | 229 | an32s 642 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
231 | 230 | expr 450 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
232 | 231 | reximdva 3197 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧
∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
233 | 232 | ex 403 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑥 ∈ (𝑤 ∩ 𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
234 | 195, 233 | syld 47 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
235 | 234 | com23 86 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑘 ∈ ℝ
(𝑘(,]+∞) ⊆
𝑤 → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
236 | 177, 235 | syl5 34 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ (𝑤
∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)))) |
237 | 236 | impl 449 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
∧ +∞ ∈ (𝑤
∩ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
238 | 237 | expimpd 447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ ))
→ ((+∞ ∈ (𝑤
∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
239 | 238 | rexlimdva 3212 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
240 | 239 | adantlr 705 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
(ordTop‘ ≤ )(+∞ ∈ (𝑤 ∩ 𝐴) ∧ ((𝑥 ∈ 𝐴 ↦ 𝑅) “ (𝑤 ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
241 | 173, 240 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) →
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
242 | 241 | ralrimiva 3147 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟)) |
243 | 26, 33, 14 | rlim2lt 14636 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
244 | 243 | adantr 474 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+
∃𝑘 ∈ ℝ
∀𝑥 ∈ 𝐵 (𝑘 < 𝑥 → (abs‘(𝑅 − 𝐶)) < 𝑟))) |
245 | 242, 244 | mpbird 249 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶) |
246 | 146, 245 | impbida 791 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ↦ 𝑅) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))) |