Metamath Proof Explorer

Theorem metds0

Description: If a point is in a set, its distance to the set is zero. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypothesis metdscn.f ⊒ 𝐹 = ( π‘₯ ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( π‘₯ 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion metds0 ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊒ 𝐹 = ( π‘₯ ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( π‘₯ 𝐷 𝑦 ) ) , ℝ* , < ) )
2 1 metdsf ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ) β†’ 𝐹 : 𝑋 ⟢ ( 0 [,] +∞ ) )
3 2 3adant3 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 𝐹 : 𝑋 ⟢ ( 0 [,] +∞ ) )
4 ssel2 ⊒ ( ( 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 𝐴 ∈ 𝑋 )
5 4 3adant1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 𝐴 ∈ 𝑋 )
6 3 5 ffvelcdmd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) )
7 eliccxr ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* )
8 6 7 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* )
9 8 xrleidd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝐴 ) ≀ ( 𝐹 β€˜ 𝐴 ) )
10 simp1 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
11 simp2 ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 𝑆 βŠ† 𝑋 )
12 1 metdsge ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ) β†’ ( ( 𝐹 β€˜ 𝐴 ) ≀ ( 𝐹 β€˜ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) = βˆ… ) )
13 10 11 5 8 12 syl31anc ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( ( 𝐹 β€˜ 𝐴 ) ≀ ( 𝐹 β€˜ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) = βˆ… ) )
14 9 13 mpbid ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) = βˆ… )
15 simpl3 ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ 𝐴 ∈ 𝑆 )
16 10 adantr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) )
17 5 adantr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ 𝐴 ∈ 𝑋 )
18 8 adantr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* )
19 simpr ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ 0 < ( 𝐹 β€˜ 𝐴 ) )
20 xblcntr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) ) β†’ 𝐴 ∈ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) )
21 16 17 18 19 20 syl112anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ 𝐴 ∈ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) )
22 inelcm ⊒ ( ( 𝐴 ∈ 𝑆 ∧ 𝐴 ∈ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) β†’ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) β‰  βˆ… )
23 15 21 22 syl2anc ⊒ ( ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) ∧ 0 < ( 𝐹 β€˜ 𝐴 ) ) β†’ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) β‰  βˆ… )
24 23 ex ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 0 < ( 𝐹 β€˜ 𝐴 ) β†’ ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) β‰  βˆ… ) )
25 24 necon2bd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( ( 𝑆 ∩ ( 𝐴 ( ball β€˜ 𝐷 ) ( 𝐹 β€˜ 𝐴 ) ) ) = βˆ… β†’ Β¬ 0 < ( 𝐹 β€˜ 𝐴 ) ) )
26 14 25 mpd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ Β¬ 0 < ( 𝐹 β€˜ 𝐴 ) )
27 elxrge0 ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ∧ 0 ≀ ( 𝐹 β€˜ 𝐴 ) ) )
28 27 simprbi ⊒ ( ( 𝐹 β€˜ 𝐴 ) ∈ ( 0 [,] +∞ ) β†’ 0 ≀ ( 𝐹 β€˜ 𝐴 ) )
29 6 28 syl ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 0 ≀ ( 𝐹 β€˜ 𝐴 ) )
30 0xr ⊒ 0 ∈ ℝ*
31 xrleloe ⊒ ( ( 0 ∈ ℝ* ∧ ( 𝐹 β€˜ 𝐴 ) ∈ ℝ* ) β†’ ( 0 ≀ ( 𝐹 β€˜ 𝐴 ) ↔ ( 0 < ( 𝐹 β€˜ 𝐴 ) ∨ 0 = ( 𝐹 β€˜ 𝐴 ) ) ) )
32 30 8 31 sylancr ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 0 ≀ ( 𝐹 β€˜ 𝐴 ) ↔ ( 0 < ( 𝐹 β€˜ 𝐴 ) ∨ 0 = ( 𝐹 β€˜ 𝐴 ) ) ) )
33 29 32 mpbid ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 0 < ( 𝐹 β€˜ 𝐴 ) ∨ 0 = ( 𝐹 β€˜ 𝐴 ) ) )
34 33 ord ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( Β¬ 0 < ( 𝐹 β€˜ 𝐴 ) β†’ 0 = ( 𝐹 β€˜ 𝐴 ) ) )
35 26 34 mpd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ 0 = ( 𝐹 β€˜ 𝐴 ) )
36 35 eqcomd ⊒ ( ( 𝐷 ∈ ( ∞Met β€˜ 𝑋 ) ∧ 𝑆 βŠ† 𝑋 ∧ 𝐴 ∈ 𝑆 ) β†’ ( 𝐹 β€˜ 𝐴 ) = 0 )