Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
metdscn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
3 |
|
metdscn.c |
⊢ 𝐶 = ( dist ‘ ℝ*𝑠 ) |
4 |
|
metdscn.k |
⊢ 𝐾 = ( MetOpen ‘ 𝐶 ) |
5 |
1
|
metdsf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
6 |
|
iccssxr |
⊢ ( 0 [,] +∞ ) ⊆ ℝ* |
7 |
|
fss |
⊢ ( ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ ( 0 [,] +∞ ) ⊆ ℝ* ) → 𝐹 : 𝑋 ⟶ ℝ* ) |
8 |
5 6 7
|
sylancl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ℝ* ) |
9 |
|
simprr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → 𝑟 ∈ ℝ+ ) |
10 |
8
|
ad2antrr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐹 : 𝑋 ⟶ ℝ* ) |
11 |
|
simplrl |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑧 ∈ 𝑋 ) |
12 |
10 11
|
ffvelrnd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ* ) |
13 |
|
simprl |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑤 ∈ 𝑋 ) |
14 |
10 13
|
ffvelrnd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ℝ* ) |
15 |
3
|
xrsdsval |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ* ∧ ( 𝐹 ‘ 𝑤 ) ∈ ℝ* ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) ) |
16 |
12 14 15
|
syl2anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) ) |
17 |
|
simplll |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
18 |
|
simpllr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑆 ⊆ 𝑋 ) |
19 |
|
simplrr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → 𝑟 ∈ ℝ+ ) |
20 |
|
xmetsym |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) ) |
21 |
17 13 11 20
|
syl3anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) = ( 𝑧 𝐷 𝑤 ) ) |
22 |
|
simprr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑧 𝐷 𝑤 ) < 𝑟 ) |
23 |
21 22
|
eqbrtrd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( 𝑤 𝐷 𝑧 ) < 𝑟 ) |
24 |
1 2 3 4 17 18 13 11 19 23
|
metdscnlem |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ) |
25 |
1 2 3 4 17 18 11 13 19 22
|
metdscnlem |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) |
26 |
|
breq1 |
⊢ ( ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) ) |
27 |
|
breq1 |
⊢ ( ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) = if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) → ( ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ↔ if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) ) |
28 |
26 27
|
ifboth |
⊢ ( ( ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) < 𝑟 ∧ ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) |
29 |
24 25 28
|
syl2anc |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → if ( ( 𝐹 ‘ 𝑧 ) ≤ ( 𝐹 ‘ 𝑤 ) , ( ( 𝐹 ‘ 𝑤 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑧 ) ) , ( ( 𝐹 ‘ 𝑧 ) +𝑒 -𝑒 ( 𝐹 ‘ 𝑤 ) ) ) < 𝑟 ) |
30 |
16 29
|
eqbrtrd |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ ( 𝑤 ∈ 𝑋 ∧ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) |
31 |
30
|
expr |
⊢ ( ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) |
32 |
31
|
ralrimiva |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) |
33 |
|
breq2 |
⊢ ( 𝑠 = 𝑟 → ( ( 𝑧 𝐷 𝑤 ) < 𝑠 ↔ ( 𝑧 𝐷 𝑤 ) < 𝑟 ) ) |
34 |
33
|
rspceaimv |
⊢ ( ( 𝑟 ∈ ℝ+ ∧ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑟 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) |
35 |
9 32 34
|
syl2anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑧 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+ ) ) → ∃ 𝑠 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) |
36 |
35
|
ralrimivva |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) |
37 |
|
simpl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
38 |
3
|
xrsxmet |
⊢ 𝐶 ∈ ( ∞Met ‘ ℝ* ) |
39 |
2 4
|
metcn |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐶 ∈ ( ∞Met ‘ ℝ* ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) ) ) |
40 |
37 38 39
|
sylancl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ ℝ* ∧ ∀ 𝑧 ∈ 𝑋 ∀ 𝑟 ∈ ℝ+ ∃ 𝑠 ∈ ℝ+ ∀ 𝑤 ∈ 𝑋 ( ( 𝑧 𝐷 𝑤 ) < 𝑠 → ( ( 𝐹 ‘ 𝑧 ) 𝐶 ( 𝐹 ‘ 𝑤 ) ) < 𝑟 ) ) ) ) |
41 |
8 36 40
|
mpbir2and |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |