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

Theorem xrlimcnp 26709
Description: Relate a limit of a real-valued sequence at infinity to the continuity of the corresponding extended real function at +∞. Since any β‡π‘Ÿ limit can be written in the form on the left side of the implication, this shows that real limits are a special case of topological continuity at a point. (Contributed by Mario Carneiro, 8-Sep-2015.)
Hypotheses
Ref Expression
xrlimcnp.a (πœ‘ β†’ 𝐴 = (𝐡 βˆͺ {+∞}))
xrlimcnp.b (πœ‘ β†’ 𝐡 βŠ† ℝ)
xrlimcnp.r ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑅 ∈ β„‚)
xrlimcnp.c (π‘₯ = +∞ β†’ 𝑅 = 𝐢)
xrlimcnp.j 𝐽 = (TopOpenβ€˜β„‚fld)
xrlimcnp.k 𝐾 = ((ordTopβ€˜ ≀ ) β†Ύt 𝐴)
Assertion
Ref Expression
xrlimcnp (πœ‘ β†’ ((π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)))
Distinct variable groups:   π‘₯,𝐡   πœ‘,π‘₯   π‘₯,𝐴   π‘₯,𝐢
Allowed substitution hints:   𝑅(π‘₯)   𝐽(π‘₯)   𝐾(π‘₯)

Proof of Theorem xrlimcnp
Dummy variables π‘˜ π‘Ÿ 𝑀 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrlimcnp.r . . . . 5 ((πœ‘ ∧ π‘₯ ∈ 𝐴) β†’ 𝑅 ∈ β„‚)
21fmpttd 7115 . . . 4 (πœ‘ β†’ (π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚)
32adantr 479 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ (π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚)
4 eqid 2730 . . . . . . . 8 (π‘₯ ∈ 𝐴 ↦ 𝑅) = (π‘₯ ∈ 𝐴 ↦ 𝑅)
5 xrlimcnp.c . . . . . . . 8 (π‘₯ = +∞ β†’ 𝑅 = 𝐢)
6 ssun2 4172 . . . . . . . . . 10 {+∞} βŠ† (𝐡 βˆͺ {+∞})
7 pnfex 11271 . . . . . . . . . . 11 +∞ ∈ V
87snid 4663 . . . . . . . . . 10 +∞ ∈ {+∞}
96, 8sselii 3978 . . . . . . . . 9 +∞ ∈ (𝐡 βˆͺ {+∞})
10 xrlimcnp.a . . . . . . . . 9 (πœ‘ β†’ 𝐴 = (𝐡 βˆͺ {+∞}))
119, 10eleqtrrid 2838 . . . . . . . 8 (πœ‘ β†’ +∞ ∈ 𝐴)
125eleq1d 2816 . . . . . . . . 9 (π‘₯ = +∞ β†’ (𝑅 ∈ β„‚ ↔ 𝐢 ∈ β„‚))
131ralrimiva 3144 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐴 𝑅 ∈ β„‚)
1412, 13, 11rspcdva 3612 . . . . . . . 8 (πœ‘ β†’ 𝐢 ∈ β„‚)
154, 5, 11, 14fvmptd3 7020 . . . . . . 7 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) = 𝐢)
1615ad2antrr 722 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ 𝑦 ∈ 𝐽) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) = 𝐢)
1716eleq1d 2816 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ 𝑦 ∈ 𝐽) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 ↔ 𝐢 ∈ 𝑦))
18 cnxmet 24509 . . . . . . . 8 (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚)
19 xrlimcnp.j . . . . . . . . . 10 𝐽 = (TopOpenβ€˜β„‚fld)
2019cnfldtopn 24518 . . . . . . . . 9 𝐽 = (MetOpenβ€˜(abs ∘ βˆ’ ))
2120mopni2 24222 . . . . . . . 8 (((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝑦 ∈ 𝐽 ∧ 𝐢 ∈ 𝑦) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)
2218, 21mp3an1 1446 . . . . . . 7 ((𝑦 ∈ 𝐽 ∧ 𝐢 ∈ 𝑦) β†’ βˆƒπ‘Ÿ ∈ ℝ+ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)
23 ssun1 4171 . . . . . . . . . . . . 13 𝐡 βŠ† (𝐡 βˆͺ {+∞})
2423, 10sseqtrrid 4034 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐡 βŠ† 𝐴)
25 ssralv 4049 . . . . . . . . . . . 12 (𝐡 βŠ† 𝐴 β†’ (βˆ€π‘₯ ∈ 𝐴 𝑅 ∈ β„‚ β†’ βˆ€π‘₯ ∈ 𝐡 𝑅 ∈ β„‚))
2624, 13, 25sylc 65 . . . . . . . . . . 11 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐡 𝑅 ∈ β„‚)
2726ad2antrr 722 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ βˆ€π‘₯ ∈ 𝐡 𝑅 ∈ β„‚)
28 simprl 767 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ π‘Ÿ ∈ ℝ+)
29 simplr 765 . . . . . . . . . 10 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢)
3027, 28, 29rlimi 15461 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
31 letop 22930 . . . . . . . . . . . . . 14 (ordTopβ€˜ ≀ ) ∈ Top
32 xrlimcnp.b . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐡 βŠ† ℝ)
33 ressxr 11262 . . . . . . . . . . . . . . . . . . 19 ℝ βŠ† ℝ*
3432, 33sstrdi 3993 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐡 βŠ† ℝ*)
35 pnfxr 11272 . . . . . . . . . . . . . . . . . . . 20 +∞ ∈ ℝ*
3635a1i 11 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ +∞ ∈ ℝ*)
3736snssd 4811 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ {+∞} βŠ† ℝ*)
3834, 37unssd 4185 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (𝐡 βˆͺ {+∞}) βŠ† ℝ*)
3910, 38eqsstrd 4019 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐴 βŠ† ℝ*)
40 xrex 12975 . . . . . . . . . . . . . . . . 17 ℝ* ∈ V
4140ssex 5320 . . . . . . . . . . . . . . . 16 (𝐴 βŠ† ℝ* β†’ 𝐴 ∈ V)
4239, 41syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐴 ∈ V)
4342ad2antrr 722 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ 𝐴 ∈ V)
44 iocpnfordt 22939 . . . . . . . . . . . . . . 15 (π‘˜(,]+∞) ∈ (ordTopβ€˜ ≀ )
4544a1i 11 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (π‘˜(,]+∞) ∈ (ordTopβ€˜ ≀ ))
46 elrestr 17378 . . . . . . . . . . . . . 14 (((ordTopβ€˜ ≀ ) ∈ Top ∧ 𝐴 ∈ V ∧ (π‘˜(,]+∞) ∈ (ordTopβ€˜ ≀ )) β†’ ((π‘˜(,]+∞) ∩ 𝐴) ∈ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
4731, 43, 45, 46mp3an2i 1464 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘˜(,]+∞) ∩ 𝐴) ∈ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
48 xrlimcnp.k . . . . . . . . . . . . 13 𝐾 = ((ordTopβ€˜ ≀ ) β†Ύt 𝐴)
4947, 48eleqtrrdi 2842 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘˜(,]+∞) ∩ 𝐴) ∈ 𝐾)
50 simprl 767 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ π‘˜ ∈ ℝ)
5150rexrd 11268 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ π‘˜ ∈ ℝ*)
5235a1i 11 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ +∞ ∈ ℝ*)
5350ltpnfd 13105 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ π‘˜ < +∞)
54 ubioc1 13381 . . . . . . . . . . . . . 14 ((π‘˜ ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ π‘˜ < +∞) β†’ +∞ ∈ (π‘˜(,]+∞))
5551, 52, 53, 54syl3anc 1369 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ +∞ ∈ (π‘˜(,]+∞))
5611ad2antrr 722 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ +∞ ∈ 𝐴)
5755, 56elind 4193 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ +∞ ∈ ((π‘˜(,]+∞) ∩ 𝐴))
58 simplr 765 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ π‘˜ ∈ ℝ)
5958rexrd 11268 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ π‘˜ ∈ ℝ*)
60 elioc1 13370 . . . . . . . . . . . . . . . . . . . . . . . 24 ((π‘˜ ∈ ℝ* ∧ +∞ ∈ ℝ*) β†’ (π‘₯ ∈ (π‘˜(,]+∞) ↔ (π‘₯ ∈ ℝ* ∧ π‘˜ < π‘₯ ∧ π‘₯ ≀ +∞)))
6159, 35, 60sylancl 584 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ ∈ (π‘˜(,]+∞) ↔ (π‘₯ ∈ ℝ* ∧ π‘˜ < π‘₯ ∧ π‘₯ ≀ +∞)))
62 simp2 1135 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘₯ ∈ ℝ* ∧ π‘˜ < π‘₯ ∧ π‘₯ ≀ +∞) β†’ π‘˜ < π‘₯)
6361, 62syl6bi 252 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ ∈ (π‘˜(,]+∞) β†’ π‘˜ < π‘₯))
6432ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) β†’ 𝐡 βŠ† ℝ)
6564sselda 3981 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ π‘₯ ∈ ℝ)
66 ltle 11306 . . . . . . . . . . . . . . . . . . . . . . 23 ((π‘˜ ∈ ℝ ∧ π‘₯ ∈ ℝ) β†’ (π‘˜ < π‘₯ β†’ π‘˜ ≀ π‘₯))
6758, 65, 66syl2anc 582 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (π‘˜ < π‘₯ β†’ π‘˜ ≀ π‘₯))
6863, 67syld 47 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (π‘₯ ∈ (π‘˜(,]+∞) β†’ π‘˜ ≀ π‘₯))
6918a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
70 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ π‘Ÿ ∈ ℝ+)
7170ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ π‘Ÿ ∈ ℝ+)
72 rpxr 12987 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ*)
7371, 72syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ π‘Ÿ ∈ ℝ*)
7414ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ 𝐢 ∈ β„‚)
7526ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) β†’ βˆ€π‘₯ ∈ 𝐡 𝑅 ∈ β„‚)
7675r19.21bi 3246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ 𝑅 ∈ β„‚)
77 elbl3 24118 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ π‘Ÿ ∈ ℝ*) ∧ (𝐢 ∈ β„‚ ∧ 𝑅 ∈ β„‚)) β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ (𝑅(abs ∘ βˆ’ )𝐢) < π‘Ÿ))
7869, 73, 74, 76, 77syl22anc 835 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ (𝑅(abs ∘ βˆ’ )𝐢) < π‘Ÿ))
79 eqid 2730 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (abs ∘ βˆ’ ) = (abs ∘ βˆ’ )
8079cnmetdval 24507 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑅 ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝑅(abs ∘ βˆ’ )𝐢) = (absβ€˜(𝑅 βˆ’ 𝐢)))
8176, 74, 80syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (𝑅(abs ∘ βˆ’ )𝐢) = (absβ€˜(𝑅 βˆ’ 𝐢)))
8281breq1d 5157 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ ((𝑅(abs ∘ βˆ’ )𝐢) < π‘Ÿ ↔ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
8378, 82bitrd 278 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
8483biimprd 247 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ ((absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
8568, 84imim12d 81 . . . . . . . . . . . . . . . . . . . 20 ((((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) ∧ π‘₯ ∈ 𝐡) β†’ ((π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ) β†’ (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
8685ralimdva 3165 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ π‘˜ ∈ ℝ) β†’ (βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ) β†’ βˆ€π‘₯ ∈ 𝐡 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
8786impr 453 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ βˆ€π‘₯ ∈ 𝐡 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
8814ad2antrr 722 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ 𝐢 ∈ β„‚)
89 simplrl 773 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ π‘Ÿ ∈ ℝ+)
90 blcntr 24139 . . . . . . . . . . . . . . . . . . . . 21 (((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝐢 ∈ β„‚ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
9118, 88, 89, 90mp3an2i 1464 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
9291a1d 25 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (+∞ ∈ (π‘˜(,]+∞) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
93 eleq1 2819 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = +∞ β†’ (π‘₯ ∈ (π‘˜(,]+∞) ↔ +∞ ∈ (π‘˜(,]+∞)))
945eleq1d 2816 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = +∞ β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
9593, 94imbi12d 343 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = +∞ β†’ ((π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ (+∞ ∈ (π‘˜(,]+∞) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
967, 95ralsn 4684 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ {+∞} (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ (+∞ ∈ (π‘˜(,]+∞) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
9792, 96sylibr 233 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ βˆ€π‘₯ ∈ {+∞} (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
98 ralunb 4190 . . . . . . . . . . . . . . . . . 18 (βˆ€π‘₯ ∈ (𝐡 βˆͺ {+∞})(π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ (βˆ€π‘₯ ∈ 𝐡 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ∧ βˆ€π‘₯ ∈ {+∞} (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
9987, 97, 98sylanbrc 581 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ βˆ€π‘₯ ∈ (𝐡 βˆͺ {+∞})(π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
10010ad2antrr 722 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ 𝐴 = (𝐡 βˆͺ {+∞}))
101100raleqdv 3323 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (βˆ€π‘₯ ∈ 𝐴 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ βˆ€π‘₯ ∈ (𝐡 βˆͺ {+∞})(π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
10299, 101mpbird 256 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ βˆ€π‘₯ ∈ 𝐴 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
103 ss2rab 4067 . . . . . . . . . . . . . . . 16 ({π‘₯ ∈ 𝐴 ∣ π‘₯ ∈ (π‘˜(,]+∞)} βŠ† {π‘₯ ∈ 𝐴 ∣ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)} ↔ βˆ€π‘₯ ∈ 𝐴 (π‘₯ ∈ (π‘˜(,]+∞) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
104102, 103sylibr 233 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ {π‘₯ ∈ 𝐴 ∣ π‘₯ ∈ (π‘˜(,]+∞)} βŠ† {π‘₯ ∈ 𝐴 ∣ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)})
105 incom 4200 . . . . . . . . . . . . . . . 16 ((π‘˜(,]+∞) ∩ 𝐴) = (𝐴 ∩ (π‘˜(,]+∞))
106 dfin5 3955 . . . . . . . . . . . . . . . 16 (𝐴 ∩ (π‘˜(,]+∞)) = {π‘₯ ∈ 𝐴 ∣ π‘₯ ∈ (π‘˜(,]+∞)}
107105, 106eqtri 2758 . . . . . . . . . . . . . . 15 ((π‘˜(,]+∞) ∩ 𝐴) = {π‘₯ ∈ 𝐴 ∣ π‘₯ ∈ (π‘˜(,]+∞)}
1084mptpreima 6236 . . . . . . . . . . . . . . 15 (β—‘(π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) = {π‘₯ ∈ 𝐴 ∣ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)}
109104, 107, 1083sstr4g 4026 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘˜(,]+∞) ∩ 𝐴) βŠ† (β—‘(π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
110 funmpt 6585 . . . . . . . . . . . . . . 15 Fun (π‘₯ ∈ 𝐴 ↦ 𝑅)
111 inss2 4228 . . . . . . . . . . . . . . . 16 ((π‘˜(,]+∞) ∩ 𝐴) βŠ† 𝐴
1122ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚)
113112fdmd 6727 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ dom (π‘₯ ∈ 𝐴 ↦ 𝑅) = 𝐴)
114111, 113sseqtrrid 4034 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘˜(,]+∞) ∩ 𝐴) βŠ† dom (π‘₯ ∈ 𝐴 ↦ 𝑅))
115 funimass3 7054 . . . . . . . . . . . . . . 15 ((Fun (π‘₯ ∈ 𝐴 ↦ 𝑅) ∧ ((π‘˜(,]+∞) ∩ 𝐴) βŠ† dom (π‘₯ ∈ 𝐴 ↦ 𝑅)) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ((π‘˜(,]+∞) ∩ 𝐴) βŠ† (β—‘(π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
116110, 114, 115sylancr 585 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ((π‘˜(,]+∞) ∩ 𝐴) βŠ† (β—‘(π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
117109, 116mpbird 256 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
118 simplrr 774 . . . . . . . . . . . . 13 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)
119117, 118sstrd 3991 . . . . . . . . . . . 12 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† 𝑦)
120 eleq2 2820 . . . . . . . . . . . . . 14 (𝑧 = ((π‘˜(,]+∞) ∩ 𝐴) β†’ (+∞ ∈ 𝑧 ↔ +∞ ∈ ((π‘˜(,]+∞) ∩ 𝐴)))
121 imaeq2 6054 . . . . . . . . . . . . . . 15 (𝑧 = ((π‘˜(,]+∞) ∩ 𝐴) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) = ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)))
122121sseq1d 4012 . . . . . . . . . . . . . 14 (𝑧 = ((π‘˜(,]+∞) ∩ 𝐴) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦 ↔ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† 𝑦))
123120, 122anbi12d 629 . . . . . . . . . . . . 13 (𝑧 = ((π‘˜(,]+∞) ∩ 𝐴) β†’ ((+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦) ↔ (+∞ ∈ ((π‘˜(,]+∞) ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† 𝑦)))
124123rspcev 3611 . . . . . . . . . . . 12 ((((π‘˜(,]+∞) ∩ 𝐴) ∈ 𝐾 ∧ (+∞ ∈ ((π‘˜(,]+∞) ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ ((π‘˜(,]+∞) ∩ 𝐴)) βŠ† 𝑦)) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦))
12549, 57, 119, 124syl12anc 833 . . . . . . . . . . 11 (((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) ∧ (π‘˜ ∈ ℝ ∧ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦))
126125rexlimdvaa 3154 . . . . . . . . . 10 ((πœ‘ ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ (βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
127126adantlr 711 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ (βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ ≀ π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
12830, 127mpd 15 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ (π‘Ÿ ∈ ℝ+ ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦)) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦))
129128rexlimdvaa 3154 . . . . . . 7 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ (βˆƒπ‘Ÿ ∈ ℝ+ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) βŠ† 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
13022, 129syl5 34 . . . . . 6 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ ((𝑦 ∈ 𝐽 ∧ 𝐢 ∈ 𝑦) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
131130expdimp 451 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ 𝑦 ∈ 𝐽) β†’ (𝐢 ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
13217, 131sylbid 239 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) ∧ 𝑦 ∈ 𝐽) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
133132ralrimiva 3144 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ βˆ€π‘¦ ∈ 𝐽 (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))
134 letopon 22929 . . . . . . 7 (ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜β„*)
135 resttopon 22885 . . . . . . 7 (((ordTopβ€˜ ≀ ) ∈ (TopOnβ€˜β„*) ∧ 𝐴 βŠ† ℝ*) β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) ∈ (TopOnβ€˜π΄))
136134, 39, 135sylancr 585 . . . . . 6 (πœ‘ β†’ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) ∈ (TopOnβ€˜π΄))
13748, 136eqeltrid 2835 . . . . 5 (πœ‘ β†’ 𝐾 ∈ (TopOnβ€˜π΄))
13819cnfldtopon 24519 . . . . . 6 𝐽 ∈ (TopOnβ€˜β„‚)
139138a1i 11 . . . . 5 (πœ‘ β†’ 𝐽 ∈ (TopOnβ€˜β„‚))
140 iscnp 22961 . . . . 5 ((𝐾 ∈ (TopOnβ€˜π΄) ∧ 𝐽 ∈ (TopOnβ€˜β„‚) ∧ +∞ ∈ 𝐴) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞) ↔ ((π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚ ∧ βˆ€π‘¦ ∈ 𝐽 (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))))
141137, 139, 11, 140syl3anc 1369 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞) ↔ ((π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚ ∧ βˆ€π‘¦ ∈ 𝐽 (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))))
142141adantr 479 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞) ↔ ((π‘₯ ∈ 𝐴 ↦ 𝑅):π΄βŸΆβ„‚ ∧ βˆ€π‘¦ ∈ 𝐽 (((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ 𝑦 β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† 𝑦)))))
1433, 133, 142mpbir2and 709 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢) β†’ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞))
144 simplr 765 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞))
14514ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐢 ∈ β„‚)
14672adantl 480 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ*)
14720blopn 24229 . . . . . . . 8 (((abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚) ∧ 𝐢 ∈ β„‚ ∧ π‘Ÿ ∈ ℝ*) β†’ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∈ 𝐽)
14818, 145, 146, 147mp3an2i 1464 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∈ 𝐽)
14915ad2antrr 722 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) = 𝐢)
150 simpr 483 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ+)
15118, 145, 150, 90mp3an2i 1464 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐢 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
152149, 151eqeltrd 2831 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
153 cnpimaex 22980 . . . . . . 7 (((π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞) ∧ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ∈ 𝐽 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅)β€˜+∞) ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
154144, 148, 152, 153syl3anc 1369 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
155 vex 3476 . . . . . . . . 9 𝑀 ∈ V
156155inex1 5316 . . . . . . . 8 (𝑀 ∩ 𝐴) ∈ V
157156a1i 11 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑀 ∈ (ordTopβ€˜ ≀ )) β†’ (𝑀 ∩ 𝐴) ∈ V)
15848eleq2i 2823 . . . . . . . 8 (𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴))
15942ad2antrr 722 . . . . . . . . 9 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐴 ∈ V)
160 elrest 17377 . . . . . . . . 9 (((ordTopβ€˜ ≀ ) ∈ Top ∧ 𝐴 ∈ V) β†’ (𝑧 ∈ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) ↔ βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )𝑧 = (𝑀 ∩ 𝐴)))
16131, 159, 160sylancr 585 . . . . . . . 8 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑧 ∈ ((ordTopβ€˜ ≀ ) β†Ύt 𝐴) ↔ βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )𝑧 = (𝑀 ∩ 𝐴)))
162158, 161bitrid 282 . . . . . . 7 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (𝑧 ∈ 𝐾 ↔ βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )𝑧 = (𝑀 ∩ 𝐴)))
163 eleq2 2820 . . . . . . . . 9 (𝑧 = (𝑀 ∩ 𝐴) β†’ (+∞ ∈ 𝑧 ↔ +∞ ∈ (𝑀 ∩ 𝐴)))
164 imaeq2 6054 . . . . . . . . . 10 (𝑧 = (𝑀 ∩ 𝐴) β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) = ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)))
165164sseq1d 4012 . . . . . . . . 9 (𝑧 = (𝑀 ∩ 𝐴) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
166163, 165anbi12d 629 . . . . . . . 8 (𝑧 = (𝑀 ∩ 𝐴) β†’ ((+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ (+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
167166adantl 480 . . . . . . 7 ((((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑧 = (𝑀 ∩ 𝐴)) β†’ ((+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ (+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
168157, 162, 167rexxfr2d 5408 . . . . . 6 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘§ ∈ 𝐾 (+∞ ∈ 𝑧 ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ 𝑧) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )(+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
169154, 168mpbid 231 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )(+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
170 elinel1 4194 . . . . . . . . . . 11 (+∞ ∈ (𝑀 ∩ 𝐴) β†’ +∞ ∈ 𝑀)
171 pnfnei 22944 . . . . . . . . . . 11 ((𝑀 ∈ (ordTopβ€˜ ≀ ) ∧ +∞ ∈ 𝑀) β†’ βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀)
172170, 171sylan2 591 . . . . . . . . . 10 ((𝑀 ∈ (ordTopβ€˜ ≀ ) ∧ +∞ ∈ (𝑀 ∩ 𝐴)) β†’ βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀)
173 df-ima 5688 . . . . . . . . . . . . . . . 16 ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) = ran ((π‘₯ ∈ 𝐴 ↦ 𝑅) β†Ύ (𝑀 ∩ 𝐴))
174 inss2 4228 . . . . . . . . . . . . . . . . . 18 (𝑀 ∩ 𝐴) βŠ† 𝐴
175 resmpt 6036 . . . . . . . . . . . . . . . . . 18 ((𝑀 ∩ 𝐴) βŠ† 𝐴 β†’ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β†Ύ (𝑀 ∩ 𝐴)) = (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅))
176174, 175ax-mp 5 . . . . . . . . . . . . . . . . 17 ((π‘₯ ∈ 𝐴 ↦ 𝑅) β†Ύ (𝑀 ∩ 𝐴)) = (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)
177176rneqi 5935 . . . . . . . . . . . . . . . 16 ran ((π‘₯ ∈ 𝐴 ↦ 𝑅) β†Ύ (𝑀 ∩ 𝐴)) = ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)
178173, 177eqtri 2758 . . . . . . . . . . . . . . 15 ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) = ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)
179178sseq1i 4009 . . . . . . . . . . . . . 14 (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
180 dfss3 3969 . . . . . . . . . . . . . 14 (ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆ€π‘§ ∈ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
181179, 180bitri 274 . . . . . . . . . . . . 13 (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆ€π‘§ ∈ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))
18213adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆ€π‘₯ ∈ 𝐴 𝑅 ∈ β„‚)
183 ssralv 4049 . . . . . . . . . . . . . . . 16 ((𝑀 ∩ 𝐴) βŠ† 𝐴 β†’ (βˆ€π‘₯ ∈ 𝐴 𝑅 ∈ β„‚ β†’ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ β„‚))
184174, 182, 183mpsyl 68 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ β„‚)
185 eqid 2730 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅) = (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)
186 eleq1 2819 . . . . . . . . . . . . . . . 16 (𝑧 = 𝑅 β†’ (𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
187185, 186ralrnmptw 7094 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ β„‚ β†’ (βˆ€π‘§ ∈ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
188184, 187syl 17 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆ€π‘§ ∈ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
189188biimpd 228 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆ€π‘§ ∈ ran (π‘₯ ∈ (𝑀 ∩ 𝐴) ↦ 𝑅)𝑧 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
190181, 189biimtrid 241 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)))
191 simplrr 774 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (π‘˜(,]+∞) βŠ† 𝑀)
19234ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ 𝐡 βŠ† ℝ*)
193 simprl 767 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ 𝐡)
194192, 193sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ ℝ*)
195 simprr 769 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘˜ < π‘₯)
196 pnfge 13114 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (π‘₯ ∈ ℝ* β†’ π‘₯ ≀ +∞)
197194, 196syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ≀ +∞)
198 simplrl 773 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘˜ ∈ ℝ)
199198rexrd 11268 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘˜ ∈ ℝ*)
200199, 35, 60sylancl 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (π‘₯ ∈ (π‘˜(,]+∞) ↔ (π‘₯ ∈ ℝ* ∧ π‘˜ < π‘₯ ∧ π‘₯ ≀ +∞)))
201194, 195, 197, 200mpbir3and 1340 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ (π‘˜(,]+∞))
202191, 201sseldd 3982 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ 𝑀)
20324ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ 𝐡 βŠ† 𝐴)
204203sselda 3981 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ π‘₯ ∈ 𝐡) β†’ π‘₯ ∈ 𝐴)
205204adantrr 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ 𝐴)
206202, 205elind 4193 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘₯ ∈ (𝑀 ∩ 𝐴))
207206ex 411 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯) β†’ π‘₯ ∈ (𝑀 ∩ 𝐴)))
208207imim1d 82 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ ((π‘₯ ∈ (𝑀 ∩ 𝐴) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ))))
20918a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (abs ∘ βˆ’ ) ∈ (∞Metβ€˜β„‚))
21072adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ*)
211210ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ π‘Ÿ ∈ ℝ*)
21214ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ 𝐢 ∈ β„‚)
21326ad2antrr 722 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ βˆ€π‘₯ ∈ 𝐡 𝑅 ∈ β„‚)
214213r19.21bi 3246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ π‘₯ ∈ 𝐡) β†’ 𝑅 ∈ β„‚)
215214adantrr 713 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ 𝑅 ∈ β„‚)
216209, 211, 212, 215, 77syl22anc 835 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ (𝑅(abs ∘ βˆ’ )𝐢) < π‘Ÿ))
217215, 212, 80syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . 23 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (𝑅(abs ∘ βˆ’ )𝐢) = (absβ€˜(𝑅 βˆ’ 𝐢)))
218217breq1d 5157 . . . . . . . . . . . . . . . . . . . . . 22 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ ((𝑅(abs ∘ βˆ’ )𝐢) < π‘Ÿ ↔ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
219216, 218bitrd 278 . . . . . . . . . . . . . . . . . . . . 21 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ (π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯)) β†’ (𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) ↔ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
220219pm5.74da 800 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ (((π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ↔ ((π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯) β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
221208, 220sylibd 238 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ ((π‘₯ ∈ (𝑀 ∩ 𝐴) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ ((π‘₯ ∈ 𝐡 ∧ π‘˜ < π‘₯) β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
222221exp4a 430 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ ((π‘₯ ∈ (𝑀 ∩ 𝐴) β†’ 𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ (π‘₯ ∈ 𝐡 β†’ (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))))
223222ralimdv2 3161 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ (βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
224223imp 405 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) ∧ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
225224an32s 648 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ∧ (π‘˜ ∈ ℝ ∧ (π‘˜(,]+∞) βŠ† 𝑀)) β†’ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
226225expr 455 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) ∧ π‘˜ ∈ ℝ) β†’ ((π‘˜(,]+∞) βŠ† 𝑀 β†’ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
227226reximdva 3166 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ (βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀 β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
228227ex 411 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆ€π‘₯ ∈ (𝑀 ∩ 𝐴)𝑅 ∈ (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ (βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀 β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))))
229190, 228syld 47 . . . . . . . . . . 11 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ (βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀 β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))))
230229com23 86 . . . . . . . . . 10 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘˜ ∈ ℝ (π‘˜(,]+∞) βŠ† 𝑀 β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))))
231172, 230syl5 34 . . . . . . . . 9 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ ((𝑀 ∈ (ordTopβ€˜ ≀ ) ∧ +∞ ∈ (𝑀 ∩ 𝐴)) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))))
232231impl 454 . . . . . . . 8 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑀 ∈ (ordTopβ€˜ ≀ )) ∧ +∞ ∈ (𝑀 ∩ 𝐴)) β†’ (((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
233232expimpd 452 . . . . . . 7 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑀 ∈ (ordTopβ€˜ ≀ )) β†’ ((+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
234233rexlimdva 3153 . . . . . 6 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )(+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
235234adantlr 711 . . . . 5 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘€ ∈ (ordTopβ€˜ ≀ )(+∞ ∈ (𝑀 ∩ 𝐴) ∧ ((π‘₯ ∈ 𝐴 ↦ 𝑅) β€œ (𝑀 ∩ 𝐴)) βŠ† (𝐢(ballβ€˜(abs ∘ βˆ’ ))π‘Ÿ)) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
236169, 235mpd 15 . . . 4 (((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
237236ralrimiva 3144 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ))
23826, 32, 14rlim2lt 15445 . . . 4 (πœ‘ β†’ ((π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢 ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
239238adantr 479 . . 3 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) β†’ ((π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢 ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘˜ ∈ ℝ βˆ€π‘₯ ∈ 𝐡 (π‘˜ < π‘₯ β†’ (absβ€˜(𝑅 βˆ’ 𝐢)) < π‘Ÿ)))
240237, 239mpbird 256 . 2 ((πœ‘ ∧ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)) β†’ (π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢)
241143, 240impbida 797 1 (πœ‘ β†’ ((π‘₯ ∈ 𝐡 ↦ 𝑅) β‡π‘Ÿ 𝐢 ↔ (π‘₯ ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)β€˜+∞)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430  Vcvv 3472   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947  {csn 4627   class class class wbr 5147   ↦ cmpt 5230  β—‘ccnv 5674  dom cdm 5675  ran crn 5676   β†Ύ cres 5677   β€œ cima 5678   ∘ ccom 5679  Fun wfun 6536  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7411  β„‚cc 11110  β„cr 11111  +∞cpnf 11249  β„*cxr 11251   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  β„+crp 12978  (,]cioc 13329  abscabs 15185   β‡π‘Ÿ crli 15433   β†Ύt crest 17370  TopOpenctopn 17371  ordTopcordt 17449  βˆžMetcxmet 21129  ballcbl 21131  β„‚fldccnfld 21144  Topctop 22615  TopOnctopon 22632   CnP ccnp 22949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-tp 4632  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-map 8824  df-pm 8825  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fi 9408  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-seq 13971  df-exp 14032  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-rlim 15437  df-struct 17084  df-slot 17119  df-ndx 17131  df-base 17149  df-plusg 17214  df-mulr 17215  df-starv 17216  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-rest 17372  df-topn 17373  df-topgen 17393  df-ordt 17451  df-ps 18523  df-tsr 18524  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cnp 22952  df-xms 24046  df-ms 24047
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator