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 [,] +∞ ) ) |