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