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 β€˜ 𝐽 ) β€˜ 𝑆 ) ) )