Theorem metdsf

Description: The distance from a point to a set is a nonnegative extended real number. (Contributed by Mario Carneiro, 14-Feb-2015) (Revised by Mario Carneiro, 4-Sep-2015) (Proof shortened by AV, 30-Sep-2020)

	Ref	Expression
Hypothesis	metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
Assertion	metdsf	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		metdscn.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
2		simplll	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3		simplr	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
4		simplr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
5	4	sselda	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑋 )
6		xmetcl	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
7	2 3 5 6	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 𝐷 𝑦 ) ∈ ℝ* )
8		eqid	⊢ ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) )
9	7 8	fmptd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) : 𝑆 ⟶ ℝ* )
10	9	frnd	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* )
11		infxrcl	⊢ ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* → inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
12	10 11	syl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* )
13		xmetge0	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
14	2 3 5 13	syl3anc	⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑆 ) → 0 ≤ ( 𝑥 𝐷 𝑦 ) )
15	14	ralrimiva	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) )
16		ovex	⊢ ( 𝑥 𝐷 𝑦 ) ∈ V
17	16	rgenw	⊢ ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐷 𝑦 ) ∈ V
18		breq2	⊢ ( 𝑧 = ( 𝑥 𝐷 𝑦 ) → ( 0 ≤ 𝑧 ↔ 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
19	8 18	ralrnmptw	⊢ ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐷 𝑦 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) ) )
20	17 19	ax-mp	⊢ ( ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 0 ≤ ( 𝑥 𝐷 𝑦 ) )
21	15 20	sylibr	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 )
22		0xr	⊢ 0 ∈ ℝ*
23		infxrgelb	⊢ ( ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) ⊆ ℝ* ∧ 0 ∈ ℝ* ) → ( 0 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ) )
24	10 22 23	sylancl	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 0 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ↔ ∀ 𝑧 ∈ ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) 0 ≤ 𝑧 ) )
25	21 24	mpbird	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
26		elxrge0	⊢ ( inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) ↔ ( inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ℝ* ∧ 0 ≤ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) )
27	12 25 26	sylanbrc	⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
28	27 1	fmptd	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )