MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xrlimcnp Structured version   Visualization version   GIF version

Theorem xrlimcnp 25552
Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any 𝑟 limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.)
Hypotheses
Ref Expression
xrlimcnp.a (𝜑𝐴 = (𝐵 ∪ {+∞}))
xrlimcnp.b (𝜑𝐵 ⊆ ℝ)
xrlimcnp.r ((𝜑𝑥𝐴) → 𝑅 ∈ ℂ)
xrlimcnp.c (𝑥 = +∞ → 𝑅 = 𝐶)
xrlimcnp.j 𝐽 = (TopOpen‘ℂfld)
xrlimcnp.k 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)
Assertion
Ref Expression
xrlimcnp (𝜑 → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))
Distinct variable groups:   𝑥,𝐵   𝜑,𝑥   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝑅(𝑥)   𝐽(𝑥)   𝐾(𝑥)

Proof of Theorem xrlimcnp
Dummy variables 𝑘 𝑟 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrlimcnp.r . . . . 5 ((𝜑𝑥𝐴) → 𝑅 ∈ ℂ)
21fmpttd 6861 . . . 4 (𝜑 → (𝑥𝐴𝑅):𝐴⟶ℂ)
32adantr 484 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (𝑥𝐴𝑅):𝐴⟶ℂ)
4 eqid 2822 . . . . . . . 8 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
5 xrlimcnp.c . . . . . . . 8 (𝑥 = +∞ → 𝑅 = 𝐶)
6 ssun2 4124 . . . . . . . . . 10 {+∞} ⊆ (𝐵 ∪ {+∞})
7 pnfex 10683 . . . . . . . . . . 11 +∞ ∈ V
87snid 4575 . . . . . . . . . 10 +∞ ∈ {+∞}
96, 8sselii 3939 . . . . . . . . 9 +∞ ∈ (𝐵 ∪ {+∞})
10 xrlimcnp.a . . . . . . . . 9 (𝜑𝐴 = (𝐵 ∪ {+∞}))
119, 10eleqtrrid 2921 . . . . . . . 8 (𝜑 → +∞ ∈ 𝐴)
125eleq1d 2898 . . . . . . . . 9 (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
131ralrimiva 3174 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴 𝑅 ∈ ℂ)
1412, 13, 11rspcdva 3600 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
154, 5, 11, 14fvmptd3 6773 . . . . . . 7 (𝜑 → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
1615ad2antrr 725 . . . . . 6 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
1716eleq1d 2898 . . . . 5 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦𝐶𝑦))
18 cnxmet 23376 . . . . . . . 8 (abs ∘ − ) ∈ (∞Met‘ℂ)
19 xrlimcnp.j . . . . . . . . . 10 𝐽 = (TopOpen‘ℂfld)
2019cnfldtopn 23385 . . . . . . . . 9 𝐽 = (MetOpen‘(abs ∘ − ))
2120mopni2 23098 . . . . . . . 8 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦𝐽𝐶𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
2218, 21mp3an1 1445 . . . . . . 7 ((𝑦𝐽𝐶𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
23 ssun1 4123 . . . . . . . . . . . . 13 𝐵 ⊆ (𝐵 ∪ {+∞})
2423, 10sseqtrrid 3995 . . . . . . . . . . . 12 (𝜑𝐵𝐴)
25 ssralv 4008 . . . . . . . . . . . 12 (𝐵𝐴 → (∀𝑥𝐴 𝑅 ∈ ℂ → ∀𝑥𝐵 𝑅 ∈ ℂ))
2624, 13, 25sylc 65 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐵 𝑅 ∈ ℂ)
2726ad2antrr 725 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∀𝑥𝐵 𝑅 ∈ ℂ)
28 simprl 770 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
29 simplr 768 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (𝑥𝐵𝑅) ⇝𝑟 𝐶)
3027, 28, 29rlimi 14861 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
31 letop 21809 . . . . . . . . . . . . . 14 (ordTop‘ ≤ ) ∈ Top
32 xrlimcnp.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ⊆ ℝ)
33 ressxr 10674 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℝ*
3432, 33sstrdi 3954 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℝ*)
35 pnfxr 10684 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
3635a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → +∞ ∈ ℝ*)
3736snssd 4715 . . . . . . . . . . . . . . . . . 18 (𝜑 → {+∞} ⊆ ℝ*)
3834, 37unssd 4137 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 ∪ {+∞}) ⊆ ℝ*)
3910, 38eqsstrd 3980 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ*)
40 xrex 12374 . . . . . . . . . . . . . . . . 17 * ∈ V
4140ssex 5201 . . . . . . . . . . . . . . . 16 (𝐴 ⊆ ℝ*𝐴 ∈ V)
4239, 41syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
4342ad2antrr 725 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐴 ∈ V)
44 iocpnfordt 21818 . . . . . . . . . . . . . . 15 (𝑘(,]+∞) ∈ (ordTop‘ ≤ )
4544a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
46 elrestr 16693 . . . . . . . . . . . . . 14 (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
4731, 43, 45, 46mp3an2i 1463 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
48 xrlimcnp.k . . . . . . . . . . . . 13 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)
4947, 48eleqtrrdi 2925 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾)
50 simprl 770 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 ∈ ℝ)
5150rexrd 10680 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*)
5235a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ ℝ*)
5350ltpnfd 12504 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 < +∞)
54 ubioc1 12778 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞))
5551, 52, 53, 54syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞))
5611ad2antrr 725 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ 𝐴)
5755, 56elind 4145 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))
58 simplr 768 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑘 ∈ ℝ)
5958rexrd 10680 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑘 ∈ ℝ*)
60 elioc1 12768 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
6159, 35, 60sylancl 589 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
62 simp2 1134 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞) → 𝑘 < 𝑥)
6361, 62syl6bi 256 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥))
6432ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ)
6564sselda 3942 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥 ∈ ℝ)
66 ltle 10718 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥𝑘𝑥))
6758, 65, 66syl2anc 587 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑘 < 𝑥𝑘𝑥))
6863, 67syld 47 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘𝑥))
6918a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
70 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
7170ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑟 ∈ ℝ+)
72 rpxr 12386 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑟 ∈ ℝ*)
7414ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ ℂ)
7526ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥𝐵 𝑅 ∈ ℂ)
7675r19.21bi 3198 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑅 ∈ ℂ)
77 elbl3 22997 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
7869, 73, 74, 76, 77syl22anc 837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
79 eqid 2822 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (abs ∘ − ) = (abs ∘ − )
8079cnmetdval 23374 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
8176, 74, 80syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
8281breq1d 5052 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅𝐶)) < 𝑟))
8378, 82bitrd 282 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅𝐶)) < 𝑟))
8483biimprd 251 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((abs‘(𝑅𝐶)) < 𝑟𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
8568, 84imim12d 81 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
8685ralimdva 3169 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
8786impr 458 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
8814ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐶 ∈ ℂ)
89 simplrl 776 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+)
90 blcntr 23018 . . . . . . . . . . . . . . . . . . . . 21 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
9118, 88, 89, 90mp3an2i 1463 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
9291a1d 25 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
93 eleq1 2901 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞)))
945eleq1d 2898 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
9593, 94imbi12d 348 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
967, 95ralsn 4593 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
9792, 96sylibr 237 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
98 ralunb 4142 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
9987, 97, 98sylanbrc 586 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
10010ad2antrr 725 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞}))
101100raleqdv 3392 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
10299, 101mpbird 260 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
103 ss2rab 4022 . . . . . . . . . . . . . . . 16 ({𝑥𝐴𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
104102, 103sylibr 237 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)})
105 incom 4152 . . . . . . . . . . . . . . . 16 ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞))
106 dfin5 3916 . . . . . . . . . . . . . . . 16 (𝐴 ∩ (𝑘(,]+∞)) = {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)}
107105, 106eqtri 2845 . . . . . . . . . . . . . . 15 ((𝑘(,]+∞) ∩ 𝐴) = {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)}
1084mptpreima 6070 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}
109104, 107, 1083sstr4g 3987 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))
110 funmpt 6372 . . . . . . . . . . . . . . 15 Fun (𝑥𝐴𝑅)
111 inss2 4180 . . . . . . . . . . . . . . . 16 ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴
1122ad2antrr 725 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝑥𝐴𝑅):𝐴⟶ℂ)
113112fdmd 6504 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → dom (𝑥𝐴𝑅) = 𝐴)
114111, 113sseqtrrid 3995 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥𝐴𝑅))
115 funimass3 6806 . . . . . . . . . . . . . . 15 ((Fun (𝑥𝐴𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥𝐴𝑅)) → (((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
116110, 114, 115sylancr 590 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
117109, 116mpbird 260 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
118 simplrr 777 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
119117, 118sstrd 3952 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)
120 eleq2 2902 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)))
121 imaeq2 5903 . . . . . . . . . . . . . . 15 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥𝐴𝑅) “ 𝑧) = ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)))
122121sseq1d 3973 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))
123120, 122anbi12d 633 . . . . . . . . . . . . 13 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)))
124123rspcev 3598 . . . . . . . . . . . 12 ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
12549, 57, 119, 124syl12anc 835 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
126125rexlimdvaa 3271 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
127126adantlr 714 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
12830, 127mpd 15 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
129128rexlimdvaa 3271 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
13022, 129syl5 34 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ((𝑦𝐽𝐶𝑦) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
131130expdimp 456 . . . . 5 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (𝐶𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
13217, 131sylbid 243 . . . 4 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
133132ralrimiva 3174 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
134 letopon 21808 . . . . . . 7 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
135 resttopon 21764 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ 𝐴 ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
136134, 39, 135sylancr 590 . . . . . 6 (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
13748, 136eqeltrid 2918 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝐴))
13819cnfldtopon 23386 . . . . . 6 𝐽 ∈ (TopOn‘ℂ)
139138a1i 11 . . . . 5 (𝜑𝐽 ∈ (TopOn‘ℂ))
140 iscnp 21840 . . . . 5 ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞ ∈ 𝐴) → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
141137, 139, 11, 140syl3anc 1368 . . . 4 (𝜑 → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
142141adantr 484 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
1433, 133, 142mpbir2and 712 . 2 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
144 simplr 768 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
14514ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ ℂ)
14672adantl 485 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
14720blopn 23105 . . . . . . . 8 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
14818, 145, 146, 147mp3an2i 1463 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
14915ad2antrr 725 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
150 simpr 488 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ+)
15118, 145, 150, 90mp3an2i 1463 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
152149, 151eqeltrd 2914 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥𝐴𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
153 cnpimaex 21859 . . . . . . 7 (((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥𝐴𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
154144, 148, 152, 153syl3anc 1368 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
155 vex 3472 . . . . . . . . 9 𝑤 ∈ V
156155inex1 5197 . . . . . . . 8 (𝑤𝐴) ∈ V
157156a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → (𝑤𝐴) ∈ V)
15848eleq2i 2905 . . . . . . . 8 (𝑧𝐾𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
15942ad2antrr 725 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V)
160 elrest 16692 . . . . . . . . 9 (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
16131, 159, 160sylancr 590 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
162158, 161syl5bb 286 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
163 eleq2 2902 . . . . . . . . 9 (𝑧 = (𝑤𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤𝐴)))
164 imaeq2 5903 . . . . . . . . . 10 (𝑧 = (𝑤𝐴) → ((𝑥𝐴𝑅) “ 𝑧) = ((𝑥𝐴𝑅) “ (𝑤𝐴)))
165164sseq1d 3973 . . . . . . . . 9 (𝑧 = (𝑤𝐴) → (((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
166163, 165anbi12d 633 . . . . . . . 8 (𝑧 = (𝑤𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
167166adantl 485 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
168157, 162, 167rexxfr2d 5289 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
169154, 168mpbid 235 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
170 elinel1 4146 . . . . . . . . . . 11 (+∞ ∈ (𝑤𝐴) → +∞ ∈ 𝑤)
171 pnfnei 21823 . . . . . . . . . . 11 ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑤) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
172170, 171sylan2 595 . . . . . . . . . 10 ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤𝐴)) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
173 df-ima 5545 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑅) “ (𝑤𝐴)) = ran ((𝑥𝐴𝑅) ↾ (𝑤𝐴))
174 inss2 4180 . . . . . . . . . . . . . . . . . 18 (𝑤𝐴) ⊆ 𝐴
175 resmpt 5883 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴) ⊆ 𝐴 → ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅))
176174, 175ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
177176rneqi 5784 . . . . . . . . . . . . . . . 16 ran ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
178173, 177eqtri 2845 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑅) “ (𝑤𝐴)) = ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
179178sseq1i 3970 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
180 dfss3 3930 . . . . . . . . . . . . . 14 (ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
181179, 180bitri 278 . . . . . . . . . . . . 13 (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
18213adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥𝐴 𝑅 ∈ ℂ)
183 ssralv 4008 . . . . . . . . . . . . . . . 16 ((𝑤𝐴) ⊆ 𝐴 → (∀𝑥𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ))
184174, 182, 183mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ)
185 eqid 2822 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
186 eleq1 2901 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
187185, 186ralrnmptw 6842 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
188184, 187syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
189188biimpd 232 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
190181, 189syl5bi 245 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
191 simplrr 777 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤)
19234ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝐵 ⊆ ℝ*)
193 simprl 770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝐵)
194192, 193sseldd 3943 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ ℝ*)
195 simprr 772 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 < 𝑥)
196 pnfge 12513 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ*𝑥 ≤ +∞)
197194, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ≤ +∞)
198 simplrl 776 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 ∈ ℝ)
199198rexrd 10680 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 ∈ ℝ*)
200199, 35, 60sylancl 589 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
201194, 195, 197, 200mpbir3and 1339 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞))
202191, 201sseldd 3943 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝑤)
20324ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵𝐴)
204203sselda 3942 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥𝐵) → 𝑥𝐴)
205204adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝐴)
206202, 205elind 4145 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ (𝑤𝐴))
207206ex 416 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥𝐵𝑘 < 𝑥) → 𝑥 ∈ (𝑤𝐴)))
208207imim1d 82 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥𝐵𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
20918a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
21072adantl 485 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
211210ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑟 ∈ ℝ*)
21214ad3antrrr 729 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝐶 ∈ ℂ)
21326ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥𝐵 𝑅 ∈ ℂ)
214213r19.21bi 3198 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥𝐵) → 𝑅 ∈ ℂ)
215214adantrr 716 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑅 ∈ ℂ)
216209, 211, 212, 215, 77syl22anc 837 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
217215, 212, 80syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
218217breq1d 5052 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅𝐶)) < 𝑟))
219216, 218bitrd 282 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅𝐶)) < 𝑟))
220219pm5.74da 803 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥𝐵𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥𝐵𝑘 < 𝑥) → (abs‘(𝑅𝐶)) < 𝑟)))
221208, 220sylibd 242 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥𝐵𝑘 < 𝑥) → (abs‘(𝑅𝐶)) < 𝑟)))
222221exp4a 435 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
223222ralimdv2 3168 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
224223imp 410 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
225224an32s 651 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
226225expr 460 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
227226reximdva 3260 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
228227ex 416 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
229190, 228syld 47 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
230229com23 86 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
231172, 230syl5 34 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤𝐴)) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
232231impl 459 . . . . . . . 8 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) ∧ +∞ ∈ (𝑤𝐴)) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
233232expimpd 457 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → ((+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
234233rexlimdva 3270 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
235234adantlr 714 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
236169, 235mpd 15 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
237236ralrimiva 3174 . . 3 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
23826, 32, 14rlim2lt 14845 . . . 4 (𝜑 → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
239238adantr 484 . . 3 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
240237, 239mpbird 260 . 2 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥𝐵𝑅) ⇝𝑟 𝐶)
241143, 240impbida 800 1 (𝜑 → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wral 3130  wrex 3131  {crab 3134  Vcvv 3469  cun 3906  cin 3907  wss 3908  {csn 4539   class class class wbr 5042  cmpt 5122  ccnv 5531  dom cdm 5532  ran crn 5533  cres 5534  cima 5535  ccom 5536  Fun wfun 6328  wf 6330  cfv 6334  (class class class)co 7140  cc 10524  cr 10525  +∞cpnf 10661  *cxr 10663   < clt 10664  cle 10665  cmin 10859  +crp 12377  (,]cioc 12727  abscabs 14584  𝑟 crli 14833  t crest 16685  TopOpenctopn 16686  ordTopcordt 16763  ∞Metcxmet 20074  ballcbl 20076  fldccnfld 20089  Topctop 21496  TopOnctopon 21513   CnP ccnp 21828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-om 7566  df-1st 7675  df-2nd 7676  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fi 8863  df-sup 8894  df-inf 8895  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-seq 13365  df-exp 13426  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-rlim 14837  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-plusg 16569  df-mulr 16570  df-starv 16571  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-rest 16687  df-topn 16688  df-topgen 16708  df-ordt 16765  df-ps 17801  df-tsr 17802  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-cnfld 20090  df-top 21497  df-topon 21514  df-topsp 21536  df-bases 21549  df-cnp 21831  df-xms 22925  df-ms 22926
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator