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 ffvelcdmd ⊒ ( ( ( 𝐷 ∈ ( ∞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 ffvelcdmd ⊒ ( ( ( 𝐷 ∈ ( ∞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 β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐡 ∈ 𝑋 ) ) β†’ ( 𝐹 β€˜ 𝐴 ) ≀ ( ( 𝐴 𝐷 𝐡 ) +𝑒 ( 𝐹 β€˜ 𝐡 ) ) )