Metamath Proof Explorer


Theorem metdstri

Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol d denotes the point-point and point-set distance functions, this theorem would be written d ( a , S ) <_ d ( a , b ) + d ( b , S ) . (Contributed by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis metdscn.f 𝐹 = ( 𝑥𝑋 ↦ inf ( ran ( 𝑦𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion metdstri ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐹𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐹𝐵 ) ) )

Proof

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 ‘ 𝑋 ) ∧ 𝑆𝑋 ) ∧ ( 𝐴𝑋𝐵𝑋 ) ) → ( 𝐹𝐴 ) ≤ ( ( 𝐴 𝐷 𝐵 ) +𝑒 ( 𝐹𝐵 ) ) )