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

Theorem xrlimcnp 24917
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 ((𝜑𝑥𝐴) → 𝑅 ∈ ℂ)
2 eqid 2771 . . . . 5 (𝑥𝐴𝑅) = (𝑥𝐴𝑅)
31, 2fmptd 6528 . . . 4 (𝜑 → (𝑥𝐴𝑅):𝐴⟶ℂ)
43adantr 466 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (𝑥𝐴𝑅):𝐴⟶ℂ)
5 ssun2 3929 . . . . . . . . . 10 {+∞} ⊆ (𝐵 ∪ {+∞})
6 pnfex 10296 . . . . . . . . . . 11 +∞ ∈ V
76snid 4348 . . . . . . . . . 10 +∞ ∈ {+∞}
85, 7sselii 3750 . . . . . . . . 9 +∞ ∈ (𝐵 ∪ {+∞})
9 xrlimcnp.a . . . . . . . . 9 (𝜑𝐴 = (𝐵 ∪ {+∞}))
108, 9syl5eleqr 2857 . . . . . . . 8 (𝜑 → +∞ ∈ 𝐴)
11 xrlimcnp.c . . . . . . . . . 10 (𝑥 = +∞ → 𝑅 = 𝐶)
1211eleq1d 2835 . . . . . . . . 9 (𝑥 = +∞ → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ))
131ralrimiva 3115 . . . . . . . . 9 (𝜑 → ∀𝑥𝐴 𝑅 ∈ ℂ)
1412, 13, 10rspcdva 3467 . . . . . . . 8 (𝜑𝐶 ∈ ℂ)
1511, 2fvmptg 6423 . . . . . . . 8 ((+∞ ∈ 𝐴𝐶 ∈ ℂ) → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
1610, 14, 15syl2anc 567 . . . . . . 7 (𝜑 → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
1716ad2antrr 699 . . . . . 6 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
1817eleq1d 2835 . . . . 5 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦𝐶𝑦))
19 cnxmet 22797 . . . . . . . 8 (abs ∘ − ) ∈ (∞Met‘ℂ)
20 xrlimcnp.j . . . . . . . . . 10 𝐽 = (TopOpen‘ℂfld)
2120cnfldtopn 22806 . . . . . . . . 9 𝐽 = (MetOpen‘(abs ∘ − ))
2221mopni2 22519 . . . . . . . 8 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑦𝐽𝐶𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
2319, 22mp3an1 1559 . . . . . . 7 ((𝑦𝐽𝐶𝑦) → ∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
24 ssun1 3928 . . . . . . . . . . . . 13 𝐵 ⊆ (𝐵 ∪ {+∞})
2524, 9syl5sseqr 3804 . . . . . . . . . . . 12 (𝜑𝐵𝐴)
26 ssralv 3816 . . . . . . . . . . . 12 (𝐵𝐴 → (∀𝑥𝐴 𝑅 ∈ ℂ → ∀𝑥𝐵 𝑅 ∈ ℂ))
2725, 13, 26sylc 65 . . . . . . . . . . 11 (𝜑 → ∀𝑥𝐵 𝑅 ∈ ℂ)
2827ad2antrr 699 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∀𝑥𝐵 𝑅 ∈ ℂ)
29 simprl 748 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
30 simplr 746 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (𝑥𝐵𝑅) ⇝𝑟 𝐶)
3128, 29, 30rlimi 14453 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
32 letop 21232 . . . . . . . . . . . . . . 15 (ordTop‘ ≤ ) ∈ Top
3332a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (ordTop‘ ≤ ) ∈ Top)
34 xrlimcnp.b . . . . . . . . . . . . . . . . . . 19 (𝜑𝐵 ⊆ ℝ)
35 ressxr 10286 . . . . . . . . . . . . . . . . . . 19 ℝ ⊆ ℝ*
3634, 35syl6ss 3765 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ⊆ ℝ*)
37 pnfxr 10295 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
3837a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝜑 → +∞ ∈ ℝ*)
3938snssd 4476 . . . . . . . . . . . . . . . . . 18 (𝜑 → {+∞} ⊆ ℝ*)
4036, 39unssd 3941 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐵 ∪ {+∞}) ⊆ ℝ*)
419, 40eqsstrd 3789 . . . . . . . . . . . . . . . 16 (𝜑𝐴 ⊆ ℝ*)
42 xrex 12033 . . . . . . . . . . . . . . . . 17 * ∈ V
4342ssex 4937 . . . . . . . . . . . . . . . 16 (𝐴 ⊆ ℝ*𝐴 ∈ V)
4441, 43syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐴 ∈ V)
4544ad2antrr 699 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐴 ∈ V)
46 iocpnfordt 21241 . . . . . . . . . . . . . . 15 (𝑘(,]+∞) ∈ (ordTop‘ ≤ )
4746a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝑘(,]+∞) ∈ (ordTop‘ ≤ ))
48 elrestr 16298 . . . . . . . . . . . . . 14 (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ (𝑘(,]+∞) ∈ (ordTop‘ ≤ )) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
4933, 45, 47, 48syl3anc 1476 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
50 xrlimcnp.k . . . . . . . . . . . . 13 𝐾 = ((ordTop‘ ≤ ) ↾t 𝐴)
5149, 50syl6eleqr 2861 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾)
52 simprl 748 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 ∈ ℝ)
5352rexrd 10292 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 ∈ ℝ*)
5437a1i 11 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ ℝ*)
55 ltpnf 12160 . . . . . . . . . . . . . . 15 (𝑘 ∈ ℝ → 𝑘 < +∞)
5652, 55syl 17 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑘 < +∞)
57 ubioc1 12433 . . . . . . . . . . . . . 14 ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*𝑘 < +∞) → +∞ ∈ (𝑘(,]+∞))
5853, 54, 56, 57syl3anc 1476 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ (𝑘(,]+∞))
5910ad2antrr 699 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ 𝐴)
6058, 59elind 3950 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴))
61 simplr 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑘 ∈ ℝ)
6261rexrd 10292 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑘 ∈ ℝ*)
63 elioc1 12423 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
6462, 37, 63sylancl 568 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
65 simp2 1131 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞) → 𝑘 < 𝑥)
6664, 65syl6bi 243 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘 < 𝑥))
6734ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → 𝐵 ⊆ ℝ)
6867sselda 3753 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑥 ∈ ℝ)
69 ltle 10329 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ) → (𝑘 < 𝑥𝑘𝑥))
7061, 68, 69syl2anc 567 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑘 < 𝑥𝑘𝑥))
7166, 70syld 47 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑥 ∈ (𝑘(,]+∞) → 𝑘𝑥))
7219a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (abs ∘ − ) ∈ (∞Met‘ℂ))
73 simprl 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → 𝑟 ∈ ℝ+)
7473ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑟 ∈ ℝ+)
75 rpxr 12044 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑟 ∈ ℝ+𝑟 ∈ ℝ*)
7674, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑟 ∈ ℝ*)
7714ad3antrrr 703 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝐶 ∈ ℂ)
7827ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → ∀𝑥𝐵 𝑅 ∈ ℂ)
7978r19.21bi 3081 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → 𝑅 ∈ ℂ)
80 elbl3 22418 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑟 ∈ ℝ*) ∧ (𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
8172, 76, 77, 79, 80syl22anc 1477 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
82 eqid 2771 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (abs ∘ − ) = (abs ∘ − )
8382cnmetdval 22795 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
8479, 77, 83syl2anc 567 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
8584breq1d 4797 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅𝐶)) < 𝑟))
8681, 85bitrd 268 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅𝐶)) < 𝑟))
8786biimprd 238 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((abs‘(𝑅𝐶)) < 𝑟𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
8871, 87imim12d 81 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) ∧ 𝑥𝐵) → ((𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
8988ralimdva 3111 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ 𝑘 ∈ ℝ) → (∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
9089impr 442 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
9119a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (abs ∘ − ) ∈ (∞Met‘ℂ))
9214ad2antrr 699 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐶 ∈ ℂ)
93 simplrl 756 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝑟 ∈ ℝ+)
94 blcntr 22439 . . . . . . . . . . . . . . . . . . . . 21 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
9591, 92, 93, 94syl3anc 1476 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
9695a1d 25 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
97 eleq1 2838 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = +∞ → (𝑥 ∈ (𝑘(,]+∞) ↔ +∞ ∈ (𝑘(,]+∞)))
9811eleq1d 2835 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = +∞ → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
9997, 98imbi12d 333 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = +∞ → ((𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
1006, 99ralsn 4361 . . . . . . . . . . . . . . . . . . 19 (∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑘(,]+∞) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
10196, 100sylibr 224 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
102 ralunb 3946 . . . . . . . . . . . . . . . . . 18 (∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (∀𝑥𝐵 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ ∀𝑥 ∈ {+∞} (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
10390, 101, 102sylanbrc 566 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
1049ad2antrr 699 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → 𝐴 = (𝐵 ∪ {+∞}))
105104raleqdv 3293 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∀𝑥 ∈ (𝐵 ∪ {+∞})(𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
106103, 105mpbird 247 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
107 ss2rab 3828 . . . . . . . . . . . . . . . 16 ({𝑥𝐴𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)} ↔ ∀𝑥𝐴 (𝑥 ∈ (𝑘(,]+∞) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
108106, 107sylibr 224 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)} ⊆ {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)})
109 incom 3957 . . . . . . . . . . . . . . . 16 ((𝑘(,]+∞) ∩ 𝐴) = (𝐴 ∩ (𝑘(,]+∞))
110 dfin5 3732 . . . . . . . . . . . . . . . 16 (𝐴 ∩ (𝑘(,]+∞)) = {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)}
111109, 110eqtri 2793 . . . . . . . . . . . . . . 15 ((𝑘(,]+∞) ∩ 𝐴) = {𝑥𝐴𝑥 ∈ (𝑘(,]+∞)}
1122mptpreima 5773 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)) = {𝑥𝐴𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)}
113108, 111, 1123sstr4g 3796 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟)))
114 funmpt 6070 . . . . . . . . . . . . . . 15 Fun (𝑥𝐴𝑅)
115 inss2 3983 . . . . . . . . . . . . . . . 16 ((𝑘(,]+∞) ∩ 𝐴) ⊆ 𝐴
1163ad2antrr 699 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝑥𝐴𝑅):𝐴⟶ℂ)
117 fdm 6192 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑅):𝐴⟶ℂ → dom (𝑥𝐴𝑅) = 𝐴)
118116, 117syl 17 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → dom (𝑥𝐴𝑅) = 𝐴)
119115, 118syl5sseqr 3804 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥𝐴𝑅))
120 funimass3 6477 . . . . . . . . . . . . . . 15 ((Fun (𝑥𝐴𝑅) ∧ ((𝑘(,]+∞) ∩ 𝐴) ⊆ dom (𝑥𝐴𝑅)) → (((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
121114, 119, 120sylancr 569 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑘(,]+∞) ∩ 𝐴) ⊆ ((𝑥𝐴𝑅) “ (𝐶(ball‘(abs ∘ − ))𝑟))))
122113, 121mpbird 247 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
123 simplrr 757 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)
124122, 123sstrd 3763 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)
125 eleq2 2839 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ ((𝑘(,]+∞) ∩ 𝐴)))
126 imaeq2 5604 . . . . . . . . . . . . . . 15 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((𝑥𝐴𝑅) “ 𝑧) = ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)))
127126sseq1d 3782 . . . . . . . . . . . . . 14 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → (((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦 ↔ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦))
128125, 127anbi12d 610 . . . . . . . . . . . . 13 (𝑧 = ((𝑘(,]+∞) ∩ 𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦) ↔ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)))
129128rspcev 3461 . . . . . . . . . . . 12 ((((𝑘(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((𝑘(,]+∞) ∩ 𝐴) ∧ ((𝑥𝐴𝑅) “ ((𝑘(,]+∞) ∩ 𝐴)) ⊆ 𝑦)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
13051, 60, 124, 129syl12anc 1474 . . . . . . . . . . 11 (((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) ∧ (𝑘 ∈ ℝ ∧ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟))) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
131130rexlimdvaa 3180 . . . . . . . . . 10 ((𝜑 ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
132131adantlr 688 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → (∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘𝑥 → (abs‘(𝑅𝐶)) < 𝑟) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
13331, 132mpd 15 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ (𝑟 ∈ ℝ+ ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦))
134133rexlimdvaa 3180 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (∃𝑟 ∈ ℝ+ (𝐶(ball‘(abs ∘ − ))𝑟) ⊆ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
13523, 134syl5 34 . . . . . 6 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ((𝑦𝐽𝐶𝑦) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
136135expdimp 440 . . . . 5 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (𝐶𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
13718, 136sylbid 230 . . . 4 (((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) ∧ 𝑦𝐽) → (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
138137ralrimiva 3115 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))
139 letopon 21231 . . . . . . 7 (ordTop‘ ≤ ) ∈ (TopOn‘ℝ*)
140 resttopon 21187 . . . . . . 7 (((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧ 𝐴 ⊆ ℝ*) → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
141139, 41, 140sylancr 569 . . . . . 6 (𝜑 → ((ordTop‘ ≤ ) ↾t 𝐴) ∈ (TopOn‘𝐴))
14250, 141syl5eqel 2854 . . . . 5 (𝜑𝐾 ∈ (TopOn‘𝐴))
14320cnfldtopon 22807 . . . . . 6 𝐽 ∈ (TopOn‘ℂ)
144143a1i 11 . . . . 5 (𝜑𝐽 ∈ (TopOn‘ℂ))
145 iscnp 21263 . . . . 5 ((𝐾 ∈ (TopOn‘𝐴) ∧ 𝐽 ∈ (TopOn‘ℂ) ∧ +∞ ∈ 𝐴) → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
146142, 144, 10, 145syl3anc 1476 . . . 4 (𝜑 → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
147146adantr 466 . . 3 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → ((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ↔ ((𝑥𝐴𝑅):𝐴⟶ℂ ∧ ∀𝑦𝐽 (((𝑥𝐴𝑅)‘+∞) ∈ 𝑦 → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ 𝑦)))))
1484, 138, 147mpbir2and 686 . 2 ((𝜑 ∧ (𝑥𝐵𝑅) ⇝𝑟 𝐶) → (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
149 simplr 746 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞))
15019a1i 11 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (abs ∘ − ) ∈ (∞Met‘ℂ))
15114ad2antrr 699 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ ℂ)
15275adantl 467 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
15321blopn 22526 . . . . . . . 8 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ*) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
154150, 151, 152, 153syl3anc 1476 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽)
15516ad2antrr 699 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥𝐴𝑅)‘+∞) = 𝐶)
156 simpr 471 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ+)
157150, 151, 156, 94syl3anc 1476 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐶 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
158155, 157eqeltrd 2850 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ((𝑥𝐴𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
159 cnpimaex 21282 . . . . . . 7 (((𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞) ∧ (𝐶(ball‘(abs ∘ − ))𝑟) ∈ 𝐽 ∧ ((𝑥𝐴𝑅)‘+∞) ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
160149, 154, 158, 159syl3anc 1476 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
161 vex 3354 . . . . . . . . 9 𝑤 ∈ V
162161inex1 4934 . . . . . . . 8 (𝑤𝐴) ∈ V
163162a1i 11 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → (𝑤𝐴) ∈ V)
16450eleq2i 2842 . . . . . . . 8 (𝑧𝐾𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴))
16544ad2antrr 699 . . . . . . . . 9 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → 𝐴 ∈ V)
166 elrest 16297 . . . . . . . . 9 (((ordTop‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
16732, 165, 166sylancr 569 . . . . . . . 8 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧 ∈ ((ordTop‘ ≤ ) ↾t 𝐴) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
168164, 167syl5bb 272 . . . . . . 7 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (𝑧𝐾 ↔ ∃𝑤 ∈ (ordTop‘ ≤ )𝑧 = (𝑤𝐴)))
169 eleq2 2839 . . . . . . . . 9 (𝑧 = (𝑤𝐴) → (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑤𝐴)))
170 imaeq2 5604 . . . . . . . . . 10 (𝑧 = (𝑤𝐴) → ((𝑥𝐴𝑅) “ 𝑧) = ((𝑥𝐴𝑅) “ (𝑤𝐴)))
171170sseq1d 3782 . . . . . . . . 9 (𝑧 = (𝑤𝐴) → (((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
172169, 171anbi12d 610 . . . . . . . 8 (𝑧 = (𝑤𝐴) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
173172adantl 467 . . . . . . 7 ((((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) ∧ 𝑧 = (𝑤𝐴)) → ((+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ (+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
174163, 168, 173rexxfr2d 5012 . . . . . 6 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑧𝐾 (+∞ ∈ 𝑧 ∧ ((𝑥𝐴𝑅) “ 𝑧) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))))
175160, 174mpbid 222 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)))
176 inss1 3982 . . . . . . . . . . . 12 (𝑤𝐴) ⊆ 𝑤
177176sseli 3749 . . . . . . . . . . 11 (+∞ ∈ (𝑤𝐴) → +∞ ∈ 𝑤)
178 pnfnei 21246 . . . . . . . . . . 11 ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ 𝑤) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
179177, 178sylan2 574 . . . . . . . . . 10 ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤𝐴)) → ∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤)
180 df-ima 5263 . . . . . . . . . . . . . . . 16 ((𝑥𝐴𝑅) “ (𝑤𝐴)) = ran ((𝑥𝐴𝑅) ↾ (𝑤𝐴))
181 inss2 3983 . . . . . . . . . . . . . . . . . 18 (𝑤𝐴) ⊆ 𝐴
182 resmpt 5591 . . . . . . . . . . . . . . . . . 18 ((𝑤𝐴) ⊆ 𝐴 → ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅))
183181, 182ax-mp 5 . . . . . . . . . . . . . . . . 17 ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
184183rneqi 5491 . . . . . . . . . . . . . . . 16 ran ((𝑥𝐴𝑅) ↾ (𝑤𝐴)) = ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
185180, 184eqtri 2793 . . . . . . . . . . . . . . 15 ((𝑥𝐴𝑅) “ (𝑤𝐴)) = ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
186185sseq1i 3779 . . . . . . . . . . . . . 14 (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟))
187 dfss3 3742 . . . . . . . . . . . . . 14 (ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
188186, 187bitri 264 . . . . . . . . . . . . 13 (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))
18913adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥𝐴 𝑅 ∈ ℂ)
190 ssralv 3816 . . . . . . . . . . . . . . . 16 ((𝑤𝐴) ⊆ 𝐴 → (∀𝑥𝐴 𝑅 ∈ ℂ → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ))
191181, 189, 190mpsyl 68 . . . . . . . . . . . . . . 15 ((𝜑𝑟 ∈ ℝ+) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ)
192 eqid 2771 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑤𝐴) ↦ 𝑅) = (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)
193 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑅 → (𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
194192, 193ralrnmpt 6512 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ ℂ → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
195191, 194syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
196195biimpd 219 . . . . . . . . . . . . 13 ((𝜑𝑟 ∈ ℝ+) → (∀𝑧 ∈ ran (𝑥 ∈ (𝑤𝐴) ↦ 𝑅)𝑧 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
197188, 196syl5bi 232 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)))
198 simplrr 757 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑘(,]+∞) ⊆ 𝑤)
19936ad3antrrr 703 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝐵 ⊆ ℝ*)
200 simprl 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝐵)
201199, 200sseldd 3754 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ ℝ*)
202 simprr 750 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 < 𝑥)
203 pnfge 12170 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 ∈ ℝ*𝑥 ≤ +∞)
204201, 203syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ≤ +∞)
205 simplrl 756 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 ∈ ℝ)
206205rexrd 10292 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑘 ∈ ℝ*)
207206, 37, 63sylancl 568 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑥 ∈ (𝑘(,]+∞) ↔ (𝑥 ∈ ℝ*𝑘 < 𝑥𝑥 ≤ +∞)))
208201, 202, 204, 207mpbir3and 1427 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ (𝑘(,]+∞))
209198, 208sseldd 3754 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝑤)
21025ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → 𝐵𝐴)
211210sselda 3753 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥𝐵) → 𝑥𝐴)
212211adantrr 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥𝐴)
213209, 212elind 3950 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑥 ∈ (𝑤𝐴))
214213ex 397 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥𝐵𝑘 < 𝑥) → 𝑥 ∈ (𝑤𝐴)))
215214imim1d 82 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥𝐵𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟))))
21619a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (abs ∘ − ) ∈ (∞Met‘ℂ))
21775adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ*)
218217ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑟 ∈ ℝ*)
21914ad3antrrr 703 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝐶 ∈ ℂ)
22027ad2antrr 699 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥𝐵 𝑅 ∈ ℂ)
221220r19.21bi 3081 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ 𝑥𝐵) → 𝑅 ∈ ℂ)
222221adantrr 690 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → 𝑅 ∈ ℂ)
223216, 218, 219, 222, 80syl22anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (𝑅(abs ∘ − )𝐶) < 𝑟))
224222, 219, 83syl2anc 567 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅𝐶)))
225224breq1d 4797 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → ((𝑅(abs ∘ − )𝐶) < 𝑟 ↔ (abs‘(𝑅𝐶)) < 𝑟))
226223, 225bitrd 268 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ (𝑥𝐵𝑘 < 𝑥)) → (𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) ↔ (abs‘(𝑅𝐶)) < 𝑟))
227226pm5.74da 799 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (((𝑥𝐵𝑘 < 𝑥) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ↔ ((𝑥𝐵𝑘 < 𝑥) → (abs‘(𝑅𝐶)) < 𝑟)))
228215, 227sylibd 229 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ((𝑥𝐵𝑘 < 𝑥) → (abs‘(𝑅𝐶)) < 𝑟)))
229228exp4a 418 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ((𝑥 ∈ (𝑤𝐴) → 𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (𝑥𝐵 → (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
230229ralimdv2 3110 . . . . . . . . . . . . . . . . 17 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
231230imp 393 . . . . . . . . . . . . . . . 16 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
232231an32s 625 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ (𝑘 ∈ ℝ ∧ (𝑘(,]+∞) ⊆ 𝑤)) → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
233232expr 444 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) ∧ 𝑘 ∈ ℝ) → ((𝑘(,]+∞) ⊆ 𝑤 → ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
234233reximdva 3165 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ ∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟)) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
235234ex 397 . . . . . . . . . . . 12 ((𝜑𝑟 ∈ ℝ+) → (∀𝑥 ∈ (𝑤𝐴)𝑅 ∈ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
236197, 235syld 47 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
237236com23 86 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (∃𝑘 ∈ ℝ (𝑘(,]+∞) ⊆ 𝑤 → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
238179, 237syl5 34 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ((𝑤 ∈ (ordTop‘ ≤ ) ∧ +∞ ∈ (𝑤𝐴)) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))))
239238impl 443 . . . . . . . 8 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) ∧ +∞ ∈ (𝑤𝐴)) → (((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
240239expimpd 441 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑤 ∈ (ordTop‘ ≤ )) → ((+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
241240rexlimdva 3179 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
242241adantlr 688 . . . . 5 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ (ordTop‘ ≤ )(+∞ ∈ (𝑤𝐴) ∧ ((𝑥𝐴𝑅) “ (𝑤𝐴)) ⊆ (𝐶(ball‘(abs ∘ − ))𝑟)) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
243175, 242mpd 15 . . . 4 (((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) ∧ 𝑟 ∈ ℝ+) → ∃𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
244243ralrimiva 3115 . . 3 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟))
24527, 34, 14rlim2lt 14437 . . . 4 (𝜑 → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
246245adantr 466 . . 3 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ ∀𝑟 ∈ ℝ+𝑘 ∈ ℝ ∀𝑥𝐵 (𝑘 < 𝑥 → (abs‘(𝑅𝐶)) < 𝑟)))
247244, 246mpbird 247 . 2 ((𝜑 ∧ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)) → (𝑥𝐵𝑅) ⇝𝑟 𝐶)
248148, 247impbida 796 1 (𝜑 → ((𝑥𝐵𝑅) ⇝𝑟 𝐶 ↔ (𝑥𝐴𝑅) ∈ ((𝐾 CnP 𝐽)‘+∞)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cun 3722  cin 3723  wss 3724  {csn 4317   class class class wbr 4787  cmpt 4864  ccnv 5249  dom cdm 5250  ran crn 5251  cres 5252  cima 5253  ccom 5254  Fun wfun 6026  wf 6028  cfv 6032  (class class class)co 6794  cc 10137  cr 10138  +∞cpnf 10274  *cxr 10276   < clt 10277  cle 10278  cmin 10469  +crp 12036  (,]cioc 12382  abscabs 14183  𝑟 crli 14425  t crest 16290  TopOpenctopn 16291  ordTopcordt 16368  ∞Metcxmt 19947  ballcbl 19949  fldccnfld 19962  Topctop 20919  TopOnctopon 20936   CnP ccnp 21251
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7097  ax-cnex 10195  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-mulcom 10203  ax-addass 10204  ax-mulass 10205  ax-distr 10206  ax-i2m1 10207  ax-1ne0 10208  ax-1rid 10209  ax-rnegex 10210  ax-rrecex 10211  ax-cnre 10212  ax-pre-lttri 10213  ax-pre-lttrn 10214  ax-pre-ltadd 10215  ax-pre-mulgt0 10216  ax-pre-sup 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-pss 3740  df-nul 4065  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5824  df-ord 5870  df-on 5871  df-lim 5872  df-suc 5873  df-iota 5995  df-fun 6034  df-fn 6035  df-f 6036  df-f1 6037  df-fo 6038  df-f1o 6039  df-fv 6040  df-riota 6755  df-ov 6797  df-oprab 6798  df-mpt2 6799  df-om 7214  df-1st 7316  df-2nd 7317  df-wrecs 7560  df-recs 7622  df-rdg 7660  df-1o 7714  df-oadd 7718  df-er 7897  df-map 8012  df-pm 8013  df-en 8111  df-dom 8112  df-sdom 8113  df-fin 8114  df-fi 8474  df-sup 8505  df-inf 8506  df-pnf 10279  df-mnf 10280  df-xr 10281  df-ltxr 10282  df-le 10283  df-sub 10471  df-neg 10472  df-div 10888  df-nn 11224  df-2 11282  df-3 11283  df-4 11284  df-5 11285  df-6 11286  df-7 11287  df-8 11288  df-9 11289  df-n0 11496  df-z 11581  df-dec 11697  df-uz 11890  df-q 11993  df-rp 12037  df-xneg 12152  df-xadd 12153  df-xmul 12154  df-ioo 12385  df-ioc 12386  df-ico 12387  df-icc 12388  df-fz 12535  df-seq 13010  df-exp 13069  df-cj 14048  df-re 14049  df-im 14050  df-sqrt 14184  df-abs 14185  df-rlim 14429  df-struct 16067  df-ndx 16068  df-slot 16069  df-base 16071  df-plusg 16163  df-mulr 16164  df-starv 16165  df-tset 16169  df-ple 16170  df-ds 16173  df-unif 16174  df-rest 16292  df-topn 16293  df-topgen 16313  df-ordt 16370  df-ps 17409  df-tsr 17410  df-psmet 19954  df-xmet 19955  df-met 19956  df-bl 19957  df-mopn 19958  df-cnfld 19963  df-top 20920  df-topon 20937  df-topsp 20959  df-bases 20972  df-cnp 21254  df-xms 22346  df-ms 22347
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator