Metamath Proof Explorer

Theorem xrlimcnp

Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +oo . Since any ~>r 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)

Ref Expression
Hypotheses xrlimcnp.a ⊢ ( 𝜑 → 𝐴 = ( 𝐵 ∪ { +∞ } ) )
xrlimcnp.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
xrlimcnp.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
xrlimcnp.c ⊢ ( 𝑥 = +∞ → 𝑅 = 𝐶 )
xrlimcnp.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
xrlimcnp.k ⊢ 𝐾 = ( ( ordTop ‘ ≤ ) ↾t 𝐴 )
Assertion xrlimcnp ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) )

Proof

Step Hyp Ref Expression
1 xrlimcnp.a ⊢ ( 𝜑 → 𝐴 = ( 𝐵 ∪ { +∞ } ) )
2 xrlimcnp.b ⊢ ( 𝜑 → 𝐵 ⊆ ℝ )
3 xrlimcnp.r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑅 ∈ ℂ )
4 xrlimcnp.c ⊢ ( 𝑥 = +∞ → 𝑅 = 𝐶 )
5 xrlimcnp.j ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
6 xrlimcnp.k ⊢ 𝐾 = ( ( ordTop ‘ ≤ ) ↾t 𝐴 )
7 3 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ )
8 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ )
9 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
10 ssun2 ⊢ { +∞ } ⊆ ( 𝐵 ∪ { +∞ } )
11 pnfex ⊢ +∞ ∈ V
12 11 snid ⊢ +∞ ∈ { +∞ }
13 10 12 sselii ⊢ +∞ ∈ ( 𝐵 ∪ { +∞ } )
14 13 1 eleqtrrid ⊢ ( 𝜑 → +∞ ∈ 𝐴 )
15 4 eleq1d ⊢ ( 𝑥 = +∞ → ( 𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ ) )
16 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ )
17 15 16 14 rspcdva ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
18 9 4 14 17 fvmptd3 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) = 𝐶 )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) = 𝐶 )
20 19 eleq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 ↔ 𝐶 ∈ 𝑦 ) )
21 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
22 5 cnfldtopn ⊢ 𝐽 = ( MetOpen ‘ ( abs ∘ − ) )
23 22 mopni2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 )
24 21 23 mp3an1 ⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦 ) → ∃ 𝑟 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 )
25 ssun1 ⊢ 𝐵 ⊆ ( 𝐵 ∪ { +∞ } )
26 25 1 sseqtrrid ⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
27 ssralv ⊢ ( 𝐵 ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ ) )
28 26 16 27 sylc ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ )
29 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ )
30 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑟 ∈ ℝ+ )
31 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 )
32 29 30 31 rlimi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
33 letop ⊢ ( ordTop ‘ ≤ ) ∈ Top
34 ressxr ⊢ ℝ ⊆ ℝ*
35 2 34 sstrdi ⊢ ( 𝜑 → 𝐵 ⊆ ℝ* )
36 pnfxr ⊢ +∞ ∈ ℝ*
37 36 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
38 37 snssd ⊢ ( 𝜑 → { +∞ } ⊆ ℝ* )
39 35 38 unssd ⊢ ( 𝜑 → ( 𝐵 ∪ { +∞ } ) ⊆ ℝ* )
40 1 39 eqsstrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ* )
41 xrex ⊢ ℝ* ∈ V
42 41 ssex ⊢ ( 𝐴 ⊆ ℝ* → 𝐴 ∈ V )
43 40 42 syl ⊢ ( 𝜑 → 𝐴 ∈ V )
44 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝐴 ∈ V )
45 iocpnfordt ⊢ ( 𝑘 (,] +∞ ) ∈ ( ordTop ‘ ≤ )
46 45 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( 𝑘 (,] +∞ ) ∈ ( ordTop ‘ ≤ ) )
47 elrestr ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ∧ ( 𝑘 (,] +∞ ) ∈ ( ordTop ‘ ≤ ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
48 33 44 46 47 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
49 48 6 eleqtrrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∈ 𝐾 )
50 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝑘 ∈ ℝ )
51 50 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝑘 ∈ ℝ* )
52 36 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → +∞ ∈ ℝ* )
53 50 ltpnfd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝑘 < +∞ )
54 ubioc1 ⊢ ( ( 𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝑘 < +∞ ) → +∞ ∈ ( 𝑘 (,] +∞ ) )
55 51 52 53 54 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → +∞ ∈ ( 𝑘 (,] +∞ ) )
56 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → +∞ ∈ 𝐴 )
57 55 56 elind ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) )
58 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ℝ )
59 58 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ℝ* )
60 elioc1 ⊢ ( ( 𝑘 ∈ ℝ* ∧ +∞ ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞ ) ) )
61 59 36 60 sylancl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞ ) ) )
62 simp2 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞ ) → 𝑘 < 𝑥 )
63 61 62 biimtrdi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑘 < 𝑥 ) )
64 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) → 𝐵 ⊆ ℝ )
65 64 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ℝ )
66 ltle ⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 < 𝑥 → 𝑘 ≤ 𝑥 ) )
67 58 65 66 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑘 < 𝑥 → 𝑘 ≤ 𝑥 ) )
68 63 67 syld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑘 ≤ 𝑥 ) )
69 21 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
70 simprl ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → 𝑟 ∈ ℝ+ )
71 70 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑟 ∈ ℝ+ )
72 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
73 71 72 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑟 ∈ ℝ* )
74 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
75 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ )
76 75 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ ℂ )
77 elbl3 ⊢ ( ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑟 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℂ ∧ 𝑅 ∈ ℂ ) ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ) )
78 69 73 74 76 77 syl22anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ) )
79 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
80 79 cnmetdval ⊢ ( ( 𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
81 76 74 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
82 81 breq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
83 78 82 bitrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
84 83 biimprd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
85 68 84 imim12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
86 85 ralimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ 𝑘 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
87 86 impr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
88 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝐶 ∈ ℂ )
89 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝑟 ∈ ℝ+ )
90 blcntr ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
91 21 88 89 90 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
92 91 a1d ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( +∞ ∈ ( 𝑘 (,] +∞ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
93 eleq1 ⊢ ( 𝑥 = +∞ → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) ↔ +∞ ∈ ( 𝑘 (,] +∞ ) ) )
94 4 eleq1d ⊢ ( 𝑥 = +∞ → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
95 93 94 imbi12d ⊢ ( 𝑥 = +∞ → ( ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑘 (,] +∞ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
96 11 95 ralsn ⊢ ( ∀ 𝑥 ∈ { +∞ } ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑘 (,] +∞ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
97 92 96 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∀ 𝑥 ∈ { +∞ } ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
98 ralunb ⊢ ( ∀ 𝑥 ∈ ( 𝐵 ∪ { +∞ } ) ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ ∀ 𝑥 ∈ { +∞ } ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
99 87 97 98 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∀ 𝑥 ∈ ( 𝐵 ∪ { +∞ } ) ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
100 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → 𝐴 = ( 𝐵 ∪ { +∞ } ) )
101 99 100 raleqtrrdv ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
102 101 ss2rabd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) } )
103 dfin5 ⊢ ( 𝐴 ∩ ( 𝑘 (,] +∞ ) ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) }
104 103 ineqcomi ⊢ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) }
105 9 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) = { 𝑥 ∈ 𝐴 ∣ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) }
106 102 104 105 3sstr4g ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
107 funmpt ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
108 inss2 ⊢ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ 𝐴
109 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ )
110 109 fdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = 𝐴 )
111 108 110 sseqtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
112 funimass3 ⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∧ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
113 107 111 112 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
114 106 113 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
115 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 )
116 114 115 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 )
117 eleq2 ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( +∞ ∈ 𝑧 ↔ +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) )
118 imaeq2 ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) )
119 118 sseq1d ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) )
120 117 119 anbi12d ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ( +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) ) )
121 120 rspcev ⊢ ( ( ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∈ 𝐾 ∧ ( +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
122 49 57 116 121 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
123 122 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
124 123 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
125 32 124 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
126 125 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
127 24 126 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ( 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
128 127 expdimp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐶 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
129 20 128 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
130 129 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
131 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
132 resttopon ⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ 𝐴 ⊆ ℝ* ) → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
133 131 40 132 sylancr ⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
134 6 133 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐴 ) )
135 5 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
136 135 a1i ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ℂ ) )
137 iscnp ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ +∞ ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
138 134 136 14 137 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
139 138 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
140 8 130 139 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) )
141 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) )
142 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
143 72 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
144 22 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ* ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
145 21 142 143 144 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
146 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) = 𝐶 )
147 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
148 21 142 147 90 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
149 146 148 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
150 cnpimaex ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
151 141 145 149 150 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
152 vex ⊢ 𝑤 ∈ V
153 152 inex1 ⊢ ( 𝑤 ∩ 𝐴 ) ∈ V
154 153 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) → ( 𝑤 ∩ 𝐴 ) ∈ V )
155 6 eleq2i ⊢ ( 𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
156 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐴 ∈ V )
157 elrest ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
158 33 156 157 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
159 155 158 bitrid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑧 ∈ 𝐾 ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
160 eleq2 ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( +∞ ∈ 𝑧 ↔ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) )
161 imaeq2 ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) )
162 161 sseq1d ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
163 160 162 anbi12d ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
164 163 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑧 = ( 𝑤 ∩ 𝐴 ) ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
165 154 159 164 rexxfr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
166 151 165 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
167 elinel1 ⊢ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) → +∞ ∈ 𝑤 )
168 pnfnei ⊢ ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ 𝑤 ) → ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
169 167 168 sylan2 ⊢ ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
170 df-ima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) = ran ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) )
171 inss2 ⊢ ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴
172 resmpt ⊢ ( ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) )
173 171 172 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
174 173 rneqi ⊢ ran ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
175 170 174 eqtri ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) = ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
176 175 sseq1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
177 dfss3 ⊢ ( ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
178 176 177 bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
179 16 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ )
180 ssralv ⊢ ( ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ ) )
181 171 179 180 mpsyl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ )
182 eqid ⊢ ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
183 eleq1 ⊢ ( 𝑧 = 𝑅 → ( 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
184 182 183 ralrnmptw ⊢ ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
185 181 184 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
186 185 biimpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
187 178 186 biimtrid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
188 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
189 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝐵 ⊆ ℝ* )
190 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝐵 )
191 189 190 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ℝ* )
192 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 < 𝑥 )
193 191 pnfged ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ≤ +∞ )
194 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 ∈ ℝ )
195 194 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 ∈ ℝ* )
196 195 36 60 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞ ) ) )
197 191 192 193 196 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ( 𝑘 (,] +∞ ) )
198 188 197 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝑤 )
199 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → 𝐵 ⊆ 𝐴 )
200 199 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
201 200 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝐴 )
202 198 201 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) )
203 202 ex ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ) )
204 203 imim1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
205 21 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
206 72 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
207 206 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑟 ∈ ℝ* )
208 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝐶 ∈ ℂ )
209 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ )
210 209 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ ℂ )
211 210 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑅 ∈ ℂ )
212 205 207 208 211 77 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ) )
213 211 208 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
214 213 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
215 212 214 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
216 215 pm5.74da ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
217 204 216 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
218 217 exp4a ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
219 218 ralimdv2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
220 219 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
221 220 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
222 221 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ 𝑘 ∈ ℝ ) → ( ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
223 222 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
224 223 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
225 187 224 syld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
226 225 com23 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
227 169 226 syl5 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
228 227 impl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
229 228 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) → ( ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
230 229 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
231 230 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
232 166 231 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
233 232 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
234 28 2 17 rlim2lt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
235 234 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
236 233 235 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 )
237 140 236 impbida ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) )