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	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion	metdsge	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑅 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2		simpl3	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → 𝐴 ∈ 𝑋 )
3	1	metdsval	⊢ ( 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )
4	2 3	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝐹 ‘ 𝐴 ) = inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) )
5	4	breq2d	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑅 ≤ ( 𝐹 ‘ 𝐴 ) ↔ 𝑅 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ) )
6		simpll1	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
7	2	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
8		simpl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → 𝑆 ⊆ 𝑋 )
9	8	sselda	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
10		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) → ( 𝐴 𝐷 𝑤 ) ∈ ℝ* )
11	6 7 9 10	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝐴 𝐷 𝑤 ) ∈ ℝ* )
12		oveq2	⊢ ( 𝑦 = 𝑤 → ( 𝐴 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑤 ) )
13	12	cbvmptv	⊢ ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) = ( 𝑤 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑤 ) )
14	11 13	fmptd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) : 𝑆 ⟶ ℝ* )
15	14	frnd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) ⊆ ℝ* )
16		simpr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → 𝑅 ∈ ℝ* )
17		infxrgelb	⊢ ( ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) ⊆ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( 𝑅 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) 𝑅 ≤ 𝑧 ) )
18	15 16 17	syl2anc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑅 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) 𝑅 ≤ 𝑧 ) )
19	16	adantr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → 𝑅 ∈ ℝ* )
20		elbl2	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝐴 𝐷 𝑤 ) < 𝑅 ) )
21	6 19 7 9 20	syl22anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝐴 𝐷 𝑤 ) < 𝑅 ) )
22		xrltnle	⊢ ( ( ( 𝐴 𝐷 𝑤 ) ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( 𝐴 𝐷 𝑤 ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ) )
23	11 19 22	syl2anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → ( ( 𝐴 𝐷 𝑤 ) < 𝑅 ↔ ¬ 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ) )
24	21 23	bitrd	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ¬ 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ) )
25	24	con2bid	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ 𝑤 ∈ 𝑆 ) → ( 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ↔ ¬ 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) )
26	25	ralbidva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( ∀ 𝑤 ∈ 𝑆 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ↔ ∀ 𝑤 ∈ 𝑆 ¬ 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) )
27		ovex	⊢ ( 𝐴 𝐷 𝑤 ) ∈ V
28	27	rgenw	⊢ ∀ 𝑤 ∈ 𝑆 ( 𝐴 𝐷 𝑤 ) ∈ V
29		breq2	⊢ ( 𝑧 = ( 𝐴 𝐷 𝑤 ) → ( 𝑅 ≤ 𝑧 ↔ 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ) )
30	13 29	ralrnmptw	⊢ ( ∀ 𝑤 ∈ 𝑆 ( 𝐴 𝐷 𝑤 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) 𝑅 ≤ 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) ) )
31	28 30	ax-mp	⊢ ( ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) 𝑅 ≤ 𝑧 ↔ ∀ 𝑤 ∈ 𝑆 𝑅 ≤ ( 𝐴 𝐷 𝑤 ) )
32		disj	⊢ ( ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ ↔ ∀ 𝑤 ∈ 𝑆 ¬ 𝑤 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) )
33	26 31 32	3bitr4g	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) 𝑅 ≤ 𝑧 ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ ) )
34	5 18 33	3bitrd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑅 ≤ ( 𝐹 ‘ 𝐴 ) ↔ ( 𝑆 ∩ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ) = ∅ ) )