Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
simprr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) |
3 |
|
simprl |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) |
4 |
|
rexsub |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) |
5 |
2 3 4
|
syl2anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) |
6 |
5
|
oveq2d |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ) |
7 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
8 |
7
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
9 |
|
simprr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
10 |
9
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐵 ∈ 𝑋 ) |
11 |
|
simprl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
12 |
11
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → 𝐴 ∈ 𝑋 ) |
13 |
2 3
|
resubcld |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ ) |
14 |
3
|
leidd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) ) |
15 |
|
xmetsym |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) ) |
16 |
7 11 9 15
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) ) |
17 |
16
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐵 𝐷 𝐴 ) ) |
18 |
17
|
eqcomd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) ) |
19 |
2
|
recnd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℂ ) |
20 |
3
|
recnd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℂ ) |
21 |
19 20
|
nncand |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) = ( 𝐴 𝐷 𝐵 ) ) |
22 |
14 18 21
|
3brtr4d |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ) |
23 |
|
blss2 |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐵 𝐷 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐴 ) − ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
24 |
8 10 12 13 2 22 23
|
syl33anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) − ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
25 |
6 24
|
eqsstrd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
26 |
25
|
expr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ) |
27 |
7
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
28 |
9
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐵 ∈ 𝑋 ) |
29 |
1
|
metdsf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
30 |
29
|
adantr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
31 |
30 11
|
ffvelrnd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ) |
32 |
|
eliccxr |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) |
33 |
31 32
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) |
34 |
33
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) |
35 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
36 |
7 11 9 35
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
37 |
36
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
38 |
37
|
xnegcld |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → -𝑒 ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
39 |
34 38
|
xaddcld |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ) |
40 |
39
|
adantrr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ) |
41 |
|
pnfxr |
⊢ +∞ ∈ ℝ* |
42 |
41
|
a1i |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → +∞ ∈ ℝ* ) |
43 |
|
pnfge |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ ) |
44 |
40 43
|
syl |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ ) |
45 |
|
ssbl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ∧ +∞ ∈ ℝ* ) ∧ ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) ) |
46 |
27 28 40 42 44 45
|
syl221anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) ) |
47 |
|
simprr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐹 ‘ 𝐴 ) = +∞ ) |
48 |
47
|
oveq2d |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ) |
49 |
11
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐴 ∈ 𝑋 ) |
50 |
|
simprl |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) |
51 |
|
xblpnf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) ) |
52 |
27 49 51
|
syl2anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ↔ ( 𝐵 ∈ 𝑋 ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) ) ) |
53 |
28 50 52
|
mpbir2and |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ) |
54 |
|
blpnfctr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) ) |
55 |
27 49 53 54
|
syl3anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐴 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) ) |
56 |
48 55
|
eqtr2d |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) +∞ ) = ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
57 |
46 56
|
sseqtrd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
58 |
57
|
expr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) = +∞ → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ) |
59 |
|
elxrge0 |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) ) |
60 |
59
|
simprbi |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) ) |
61 |
31 60
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) ) |
62 |
|
ge0nemnf |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) |
63 |
33 61 62
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) |
64 |
33 63
|
jca |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) ) |
65 |
64
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) ) |
66 |
|
xrnemnf |
⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ≠ -∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∨ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) |
67 |
65 66
|
sylib |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ ∨ ( 𝐹 ‘ 𝐴 ) = +∞ ) ) |
68 |
26 58 67
|
mpjaod |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
69 |
|
pnfnlt |
⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) ) |
70 |
33 69
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) ) |
71 |
70
|
adantr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ¬ +∞ < ( 𝐹 ‘ 𝐴 ) ) |
72 |
36
|
xnegcld |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → -𝑒 ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
73 |
33 72
|
xaddcld |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ) |
74 |
|
xbln0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
75 |
7 9 73 74
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
76 |
|
xposdif |
⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
77 |
36 33 76
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ 0 < ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
78 |
75 77
|
bitr4d |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ) ) |
79 |
|
breq1 |
⊢ ( ( 𝐴 𝐷 𝐵 ) = +∞ → ( ( 𝐴 𝐷 𝐵 ) < ( 𝐹 ‘ 𝐴 ) ↔ +∞ < ( 𝐹 ‘ 𝐴 ) ) ) |
80 |
78 79
|
sylan9bb |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ≠ ∅ ↔ +∞ < ( 𝐹 ‘ 𝐴 ) ) ) |
81 |
80
|
necon1bbid |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( ¬ +∞ < ( 𝐹 ‘ 𝐴 ) ↔ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ∅ ) ) |
82 |
71 81
|
mpbid |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) = ∅ ) |
83 |
|
0ss |
⊢ ∅ ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) |
84 |
82 83
|
eqsstrdi |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ ( 𝐴 𝐷 𝐵 ) = +∞ ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
85 |
|
xmetge0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) ) |
86 |
7 11 9 85
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐴 𝐷 𝐵 ) ) |
87 |
|
ge0nemnf |
⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐴 𝐷 𝐵 ) ) → ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) |
88 |
36 86 87
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) |
89 |
36 88
|
jca |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) ) |
90 |
|
xrnemnf |
⊢ ( ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ) ↔ ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∨ ( 𝐴 𝐷 𝐵 ) = +∞ ) ) |
91 |
89 90
|
sylib |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) ∈ ℝ ∨ ( 𝐴 𝐷 𝐵 ) = +∞ ) ) |
92 |
68 84 91
|
mpjaodan |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) |
93 |
|
sslin |
⊢ ( ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ⊆ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ) |
94 |
92 93
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ) |
95 |
33
|
xrleidd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ) |
96 |
|
simplr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑆 ⊆ 𝑋 ) |
97 |
1
|
metdsge |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) ) |
98 |
7 96 11 33 97
|
syl31anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) ) |
99 |
95 98
|
mpbid |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) |
100 |
|
sseq0 |
⊢ ( ( ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) ⊆ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) |
101 |
94 99 100
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) |
102 |
1
|
metdsge |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ∧ ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ∈ ℝ* ) → ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) ) |
103 |
7 96 9 73 102
|
syl31anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝑆 ∩ ( 𝐵 ( ball ‘ 𝐷 ) ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) = ∅ ) ) |
104 |
101 103
|
mpbird |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ) |
105 |
30 9
|
ffvelrnd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ) |
106 |
|
eliccxr |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) |
107 |
105 106
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) |
108 |
|
elxrge0 |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) ) |
109 |
108
|
simprbi |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐵 ) ) |
110 |
105 109
|
syl |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 0 ≤ ( 𝐹 ‘ 𝐵 ) ) |
111 |
|
xlesubadd |
⊢ ( ( ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) ∧ ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ∧ ( 𝐴 𝐷 𝐵 ) ≠ -∞ ∧ 0 ≤ ( 𝐹 ‘ 𝐵 ) ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
112 |
33 36 107 61 88 110 111
|
syl33anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) +𝑒 -𝑒 ( 𝐴 𝐷 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ↔ ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) ) ) |
113 |
104 112
|
mpbid |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐹 ‘ 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) ) |
114 |
|
xaddcom |
⊢ ( ( ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ∧ ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐹 ‘ 𝐵 ) ) ) |
115 |
107 36 114
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝐵 ) +𝑒 ( 𝐴 𝐷 𝐵 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐹 ‘ 𝐵 ) ) ) |
116 |
113 115
|
breqtrd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐹 ‘ 𝐵 ) ) ) |