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 syl6bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( 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 100 raleqdv ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∀ 𝑥 ∈ ( 𝐵 ∪ { +∞ } ) ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
102 99 101 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
103 ss2rab ⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) } ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ ( 𝑘 (,] +∞ ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
104 102 103 sylibr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) } ⊆ { 𝑥 ∈ 𝐴 ∣ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) } )
105 incom ⊢ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 𝑘 (,] +∞ ) )
106 dfin5 ⊢ ( 𝐴 ∩ ( 𝑘 (,] +∞ ) ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) }
107 105 106 eqtri ⊢ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ ( 𝑘 (,] +∞ ) }
108 9 mptpreima ⊢ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) = { 𝑥 ∈ 𝐴 ∣ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) }
109 104 107 108 3sstr4g ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
110 funmpt ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝑅 )
111 inss2 ⊢ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ 𝐴
112 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ )
113 112 fdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) = 𝐴 )
114 111 113 sseqtrrid ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) )
115 funimass3 ⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∧ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ dom ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
116 110 114 115 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ⊆ ( ◡ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
117 109 116 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
118 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 )
119 117 118 sstrd ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 )
120 eleq2 ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( +∞ ∈ 𝑧 ↔ +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) )
121 imaeq2 ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) )
122 121 sseq1d ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) )
123 120 122 anbi12d ⊢ ( 𝑧 = ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ↔ ( +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) ) )
124 123 rspcev ⊢ ( ( ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∈ 𝐾 ∧ ( +∞ ∈ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( ( 𝑘 (,] +∞ ) ∩ 𝐴 ) ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
125 49 57 119 124 syl12anc ⊢ ( ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
126 125 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
127 126 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ( ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 ≤ 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
128 32 127 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) )
129 128 rexlimdvaa ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ∃ 𝑟 ∈ ℝ+ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ⊆ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
130 24 129 syl5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ( 𝑦 ∈ 𝐽 ∧ 𝐶 ∈ 𝑦 ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
131 130 expdimp ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( 𝐶 ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
132 20 131 sylbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) ∧ 𝑦 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
133 132 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) )
134 letopon ⊢ ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* )
135 resttopon ⊢ ( ( ( ordTop ‘ ≤ ) ∈ ( TopOn ‘ ℝ* ) ∧ 𝐴 ⊆ ℝ* ) → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
136 134 40 135 sylancr ⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ∈ ( TopOn ‘ 𝐴 ) )
137 6 136 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝐴 ) )
138 5 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
139 138 a1i ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ ℂ ) )
140 iscnp ⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ +∞ ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
141 137 139 14 140 syl3anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
142 141 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) : 𝐴 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝐽 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ 𝑦 → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ 𝑦 ) ) ) ) )
143 8 133 142 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) )
144 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) )
145 17 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
146 72 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
147 22 blopn ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝐶 ∈ ℂ ∧ 𝑟 ∈ ℝ* ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
148 21 145 146 147 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 )
149 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) = 𝐶 )
150 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
151 21 145 150 90 mp3an2i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐶 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
152 149 151 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
153 cnpimaex ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ∧ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ∈ 𝐽 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ‘ +∞ ) ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
154 144 148 152 153 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
155 vex ⊢ 𝑤 ∈ V
156 155 inex1 ⊢ ( 𝑤 ∩ 𝐴 ) ∈ V
157 156 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) → ( 𝑤 ∩ 𝐴 ) ∈ V )
158 6 eleq2i ⊢ ( 𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) )
159 43 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → 𝐴 ∈ V )
160 elrest ⊢ ( ( ( ordTop ‘ ≤ ) ∈ Top ∧ 𝐴 ∈ V ) → ( 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
161 33 159 160 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑧 ∈ ( ( ordTop ‘ ≤ ) ↾t 𝐴 ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
162 158 161 syl5bb ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( 𝑧 ∈ 𝐾 ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) 𝑧 = ( 𝑤 ∩ 𝐴 ) ) )
163 eleq2 ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( +∞ ∈ 𝑧 ↔ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) )
164 imaeq2 ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) )
165 164 sseq1d ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
166 163 165 anbi12d ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐴 ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
167 166 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑧 = ( 𝑤 ∩ 𝐴 ) ) → ( ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
168 157 162 167 rexxfr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑧 ∈ 𝐾 ( +∞ ∈ 𝑧 ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ 𝑧 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
169 154 168 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
170 elinel1 ⊢ ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) → +∞ ∈ 𝑤 )
171 pnfnei ⊢ ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ 𝑤 ) → ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
172 170 171 sylan2 ⊢ ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
173 df-ima ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) = ran ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) )
174 inss2 ⊢ ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴
175 resmpt ⊢ ( ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴 → ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) )
176 174 175 ax-mp ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
177 176 rneqi ⊢ ran ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ↾ ( 𝑤 ∩ 𝐴 ) ) = ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
178 173 177 eqtri ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) = ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
179 178 sseq1i ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
180 dfss3 ⊢ ( ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
181 179 180 bitri ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) )
182 16 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ )
183 ssralv ⊢ ( ( 𝑤 ∩ 𝐴 ) ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑅 ∈ ℂ → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ ) )
184 174 182 183 mpsyl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ )
185 eqid ⊢ ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) = ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 )
186 eleq1 ⊢ ( 𝑧 = 𝑅 → ( 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
187 185 186 ralrnmptw ⊢ ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ℂ → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
188 184 187 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
189 188 biimpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑧 ∈ ran ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ↦ 𝑅 ) 𝑧 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
190 181 189 syl5bi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) )
191 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑘 (,] +∞ ) ⊆ 𝑤 )
192 35 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝐵 ⊆ ℝ* )
193 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝐵 )
194 192 193 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ℝ* )
195 simprr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 < 𝑥 )
196 pnfge ⊢ ( 𝑥 ∈ ℝ* → 𝑥 ≤ +∞ )
197 194 196 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ≤ +∞ )
198 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 ∈ ℝ )
199 198 rexrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑘 ∈ ℝ* )
200 199 36 60 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑥 ∈ ( 𝑘 (,] +∞ ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑘 < 𝑥 ∧ 𝑥 ≤ +∞ ) ) )
201 194 195 197 200 mpbir3and ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ( 𝑘 (,] +∞ ) )
202 191 201 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝑤 )
203 26 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → 𝐵 ⊆ 𝐴 )
204 203 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐴 )
205 204 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ 𝐴 )
206 202 205 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) )
207 206 ex ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) ) )
208 207 imim1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ) )
209 21 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
210 72 adantl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ* )
211 210 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑟 ∈ ℝ* )
212 17 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝐶 ∈ ℂ )
213 28 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 𝑅 ∈ ℂ )
214 213 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ 𝑥 ∈ 𝐵 ) → 𝑅 ∈ ℂ )
215 214 adantrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → 𝑅 ∈ ℂ )
216 209 211 212 215 77 syl22anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ) )
217 215 212 80 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ( abs ∘ − ) 𝐶 ) = ( abs ‘ ( 𝑅 − 𝐶 ) ) )
218 217 breq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( ( 𝑅 ( abs ∘ − ) 𝐶 ) < 𝑟 ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
219 216 218 bitrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) ) → ( 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ↔ ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
220 219 pm5.74da ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
221 208 220 sylibd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ( 𝑥 ∈ 𝐵 ∧ 𝑘 < 𝑥 ) → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
222 221 exp4a ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ( 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) → 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
223 222 ralimdv2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
224 223 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
225 224 an32s ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ ( 𝑘 ∈ ℝ ∧ ( 𝑘 (,] +∞ ) ⊆ 𝑤 ) ) → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
226 225 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) ∧ 𝑘 ∈ ℝ ) → ( ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
227 226 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
228 227 ex ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑥 ∈ ( 𝑤 ∩ 𝐴 ) 𝑅 ∈ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
229 190 228 syld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
230 229 com23 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑘 ∈ ℝ ( 𝑘 (,] +∞ ) ⊆ 𝑤 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
231 172 230 syl5 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( 𝑤 ∈ ( ordTop ‘ ≤ ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) ) )
232 231 impl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) ∧ +∞ ∈ ( 𝑤 ∩ 𝐴 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
233 232 expimpd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑤 ∈ ( ordTop ‘ ≤ ) ) → ( ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
234 233 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
235 234 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ( ordTop ‘ ≤ ) ( +∞ ∈ ( 𝑤 ∩ 𝐴 ) ∧ ( ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) “ ( 𝑤 ∩ 𝐴 ) ) ⊆ ( 𝐶 ( ball ‘ ( abs ∘ − ) ) 𝑟 ) ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
236 169 235 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
237 236 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) )
238 28 2 17 rlim2lt ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
239 238 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑘 ∈ ℝ ∀ 𝑥 ∈ 𝐵 ( 𝑘 < 𝑥 → ( abs ‘ ( 𝑅 − 𝐶 ) ) < 𝑟 ) ) )
240 237 239 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) → ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 )
241 143 240 impbida ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑅 ) ⇝𝑟 𝐶 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝑅 ) ∈ ( ( 𝐾 CnP 𝐽 ) ‘ +∞ ) ) )