# Metamath Proof Explorer

## Theorem metdsge

Description: The distance from the point A to the set S is greater than R iff the R -ball around A misses S . (Contributed by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

Ref Expression
Hypothesis metdscn.f $⊢ F = x ∈ X ⟼ sup ran ⁡ y ∈ S ⟼ x D y ℝ * <$
Assertion metdsge $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → R ≤ F ⁡ A ↔ S ∩ A ball ⁡ D R = ∅$

### Proof

Step Hyp Ref Expression
1 metdscn.f $⊢ F = x ∈ X ⟼ sup ran ⁡ y ∈ S ⟼ x D y ℝ * <$
2 simpl3 $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → A ∈ X$
3 1 metdsval $⊢ A ∈ X → F ⁡ A = sup ran ⁡ y ∈ S ⟼ A D y ℝ * <$
4 2 3 syl $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → F ⁡ A = sup ran ⁡ y ∈ S ⟼ A D y ℝ * <$
5 4 breq2d $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → R ≤ F ⁡ A ↔ R ≤ sup ran ⁡ y ∈ S ⟼ A D y ℝ * <$
6 simpll1 $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → D ∈ ∞Met ⁡ X$
7 2 adantr $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → A ∈ X$
8 simpl2 $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → S ⊆ X$
9 8 sselda $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → w ∈ X$
10 xmetcl $⊢ D ∈ ∞Met ⁡ X ∧ A ∈ X ∧ w ∈ X → A D w ∈ ℝ *$
11 6 7 9 10 syl3anc $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → A D w ∈ ℝ *$
12 oveq2 $⊢ y = w → A D y = A D w$
13 12 cbvmptv $⊢ y ∈ S ⟼ A D y = w ∈ S ⟼ A D w$
14 11 13 fmptd $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → y ∈ S ⟼ A D y : S ⟶ ℝ *$
15 14 frnd $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → ran ⁡ y ∈ S ⟼ A D y ⊆ ℝ *$
16 simpr $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → R ∈ ℝ *$
17 infxrgelb $⊢ ran ⁡ y ∈ S ⟼ A D y ⊆ ℝ * ∧ R ∈ ℝ * → R ≤ sup ran ⁡ y ∈ S ⟼ A D y ℝ * < ↔ ∀ z ∈ ran ⁡ y ∈ S ⟼ A D y R ≤ z$
18 15 16 17 syl2anc $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → R ≤ sup ran ⁡ y ∈ S ⟼ A D y ℝ * < ↔ ∀ z ∈ ran ⁡ y ∈ S ⟼ A D y R ≤ z$
19 16 adantr $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → R ∈ ℝ *$
20 elbl2 $⊢ D ∈ ∞Met ⁡ X ∧ R ∈ ℝ * ∧ A ∈ X ∧ w ∈ X → w ∈ A ball ⁡ D R ↔ A D w < R$
21 6 19 7 9 20 syl22anc $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → w ∈ A ball ⁡ D R ↔ A D w < R$
22 xrltnle $⊢ A D w ∈ ℝ * ∧ R ∈ ℝ * → A D w < R ↔ ¬ R ≤ A D w$
23 11 19 22 syl2anc $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → A D w < R ↔ ¬ R ≤ A D w$
24 21 23 bitrd $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → w ∈ A ball ⁡ D R ↔ ¬ R ≤ A D w$
25 24 con2bid $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * ∧ w ∈ S → R ≤ A D w ↔ ¬ w ∈ A ball ⁡ D R$
26 25 ralbidva $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → ∀ w ∈ S R ≤ A D w ↔ ∀ w ∈ S ¬ w ∈ A ball ⁡ D R$
27 ovex $⊢ A D w ∈ V$
28 27 rgenw $⊢ ∀ w ∈ S A D w ∈ V$
29 breq2 $⊢ z = A D w → R ≤ z ↔ R ≤ A D w$
30 13 29 ralrnmptw $⊢ ∀ w ∈ S A D w ∈ V → ∀ z ∈ ran ⁡ y ∈ S ⟼ A D y R ≤ z ↔ ∀ w ∈ S R ≤ A D w$
31 28 30 ax-mp $⊢ ∀ z ∈ ran ⁡ y ∈ S ⟼ A D y R ≤ z ↔ ∀ w ∈ S R ≤ A D w$
32 disj $⊢ S ∩ A ball ⁡ D R = ∅ ↔ ∀ w ∈ S ¬ w ∈ A ball ⁡ D R$
33 26 31 32 3bitr4g $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → ∀ z ∈ ran ⁡ y ∈ S ⟼ A D y R ≤ z ↔ S ∩ A ball ⁡ D R = ∅$
34 5 18 33 3bitrd $⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X ∧ R ∈ ℝ * → R ≤ F ⁡ A ↔ S ∩ A ball ⁡ D R = ∅$