This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem metdseq0

Description: The distance from a point to a set is zero iff the point is in the closure set. (Contributed by Mario Carneiro, 14-Feb-2015)

Ref Expression
Hypotheses metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
Assertion metdseq0 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2 metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
3 simpll1 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
4 simprl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) → 𝑧 ∈ 𝐽 )
5 simprr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) → 𝐴 ∈ 𝑧 )
6 2 mopni2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) → ∃ 𝑟 ∈ ℝ+ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
7 3 4 5 6 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) → ∃ 𝑟 ∈ ℝ+ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
8 simprr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 )
9 8 ssrind ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) ⊆ ( 𝑧 ∩ 𝑆 ) )
10 rpgt0 ⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 )
11 0re ⊢ 0 ∈ ℝ
12 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
13 ltnle ⊢ ( ( 0 ∈ ℝ ∧ 𝑟 ∈ ℝ ) → ( 0 < 𝑟 ↔ ¬ 𝑟 ≤ 0 ) )
14 11 12 13 sylancr ⊢ ( 𝑟 ∈ ℝ+ → ( 0 < 𝑟 ↔ ¬ 𝑟 ≤ 0 ) )
15 10 14 mpbid ⊢ ( 𝑟 ∈ ℝ+ → ¬ 𝑟 ≤ 0 )
16 15 ad2antrl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ¬ 𝑟 ≤ 0 )
17 simpllr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
18 17 breq2d ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝑟 ≤ ( 𝐹 ‘ 𝐴 ) ↔ 𝑟 ≤ 0 ) )
19 3 adantr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
20 simpl2 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝑆 ⊆ 𝑋 )
21 20 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → 𝑆 ⊆ 𝑋 )
22 simpl3 ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ 𝑋 )
23 22 ad2antrr ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → 𝐴 ∈ 𝑋 )
24 rpxr ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ* )
25 24 ad2antrl ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → 𝑟 ∈ ℝ* )
26 1 metdsge ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑟 ∈ ℝ* ) → ( 𝑟 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ) = ∅ ) )
27 19 21 23 25 26 syl31anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝑟 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ) = ∅ ) )
28 18 27 bitr3d ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝑟 ≤ 0 ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ) = ∅ ) )
29 incom ⊢ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ) = ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 )
30 29 eqeq1i ⊢ ( ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ) = ∅ ↔ ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) = ∅ )
31 28 30 bitrdi ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝑟 ≤ 0 ↔ ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) = ∅ ) )
32 31 necon3bbid ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( ¬ 𝑟 ≤ 0 ↔ ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) ≠ ∅ ) )
33 16 32 mpbid ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) ≠ ∅ )
34 ssn0 ⊢ ( ( ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) ⊆ ( 𝑧 ∩ 𝑆 ) ∧ ( ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ∩ 𝑆 ) ≠ ∅ ) → ( 𝑧 ∩ 𝑆 ) ≠ ∅ )
35 9 33 34 syl2anc ⊢ ( ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) ∧ ( 𝑟 ∈ ℝ+ ∧ ( 𝐴 ( ball ‘ 𝐷 ) 𝑟 ) ⊆ 𝑧 ) ) → ( 𝑧 ∩ 𝑆 ) ≠ ∅ )
36 7 35 rexlimddv ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ ( 𝑧 ∈ 𝐽 ∧ 𝐴 ∈ 𝑧 ) ) → ( 𝑧 ∩ 𝑆 ) ≠ ∅ )
37 36 expr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) ∧ 𝑧 ∈ 𝐽 ) → ( 𝐴 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
38 37 ralrimiva ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) )
39 2 mopntopon ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
40 39 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
41 40 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
42 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
43 41 42 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐽 ∈ Top )
44 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
45 41 44 syl ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝑋 = ∪ 𝐽 )
46 20 45 sseqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝑆 ⊆ ∪ 𝐽 )
47 22 45 eleqtrd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ∪ 𝐽 )
48 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
49 48 elcls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ∪ 𝐽 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
50 43 46 47 49 syl3anc ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∀ 𝑧 ∈ 𝐽 ( 𝐴 ∈ 𝑧 → ( 𝑧 ∩ 𝑆 ) ≠ ∅ ) ) )
51 38 50 mpbird ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
52 incom ⊢ ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) = ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
53 1 metdsf ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
54 53 ffvelcdmda ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
55 54 3impa ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )
56 eliccxr ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
57 55 56 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
58 57 xrleidd ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) )
59 1 metdsge ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
60 57 59 mpdan ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ ) )
61 58 60 mpbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) = ∅ )
62 52 61 eqtrid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) = ∅ )
63 62 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) = ∅ )
64 40 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
65 64 42 syl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐽 ∈ Top )
66 simpll2 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝑆 ⊆ 𝑋 )
67 64 44 syl ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝑋 = ∪ 𝐽 )
68 66 67 sseqtrd ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝑆 ⊆ ∪ 𝐽 )
69 simplr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
70 simpll1 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
71 simpll3 ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ 𝑋 )
72 57 ad2antrr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ℝ* )
73 2 blopn ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∈ 𝐽 )
74 70 71 72 73 syl3anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∈ 𝐽 )
75 simpr ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 0 < ( 𝐹 ‘ 𝐴 ) )
76 xblcntr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
77 70 71 72 75 76 syl112anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) )
78 48 clsndisj ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∈ 𝐽 ∧ 𝐴 ∈ ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) ≠ ∅ )
79 65 68 69 74 77 78 syl32anc ⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 0 < ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) ≠ ∅ )
80 79 ex ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 0 < ( 𝐹 ‘ 𝐴 ) → ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) ≠ ∅ ) )
81 80 necon2bd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( ( 𝐴 ( ball ‘ 𝐷 ) ( 𝐹 ‘ 𝐴 ) ) ∩ 𝑆 ) = ∅ → ¬ 0 < ( 𝐹 ‘ 𝐴 ) ) )
82 63 81 mpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ¬ 0 < ( 𝐹 ‘ 𝐴 ) )
83 elxrge0 ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝐴 ) ) )
84 83 simprbi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
85 55 84 syl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → 0 ≤ ( 𝐹 ‘ 𝐴 ) )
86 0xr ⊢ 0 ∈ ℝ*
87 xrleloe ⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐴 ) ∈ ℝ* ) → ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) ) )
88 86 57 87 sylancr ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 0 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) ) )
89 85 88 mpbid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) )
90 89 adantr ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 0 < ( 𝐹 ‘ 𝐴 ) ∨ 0 = ( 𝐹 ‘ 𝐴 ) ) )
91 90 ord ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ¬ 0 < ( 𝐹 ‘ 𝐴 ) → 0 = ( 𝐹 ‘ 𝐴 ) ) )
92 82 91 mpd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → 0 = ( 𝐹 ‘ 𝐴 ) )
93 92 eqcomd ⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 )
94 51 93 impbida ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝐹 ‘ 𝐴 ) = 0 ↔ 𝐴 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )