Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
metdscn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐷 ) |
3 |
|
metnrmlem.1 |
⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
4 |
|
metnrmlem.2 |
⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |
5 |
|
metnrmlem.3 |
⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) |
6 |
|
metnrmlem.4 |
⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ ) |
7 |
|
1xr |
⊢ 1 ∈ ℝ* |
8 |
3
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
9 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ∈ ( Clsd ‘ 𝐽 ) ) |
10 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
11 |
10
|
cldss |
⊢ ( 𝑆 ∈ ( Clsd ‘ 𝐽 ) → 𝑆 ⊆ ∪ 𝐽 ) |
12 |
9 11
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ⊆ ∪ 𝐽 ) |
13 |
2
|
mopnuni |
⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 ) |
14 |
8 13
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑋 = ∪ 𝐽 ) |
15 |
12 14
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑆 ⊆ 𝑋 ) |
16 |
1
|
metdsf |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
17 |
8 15 16
|
syl2anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) ) |
18 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ∈ ( Clsd ‘ 𝐽 ) ) |
19 |
10
|
cldss |
⊢ ( 𝑇 ∈ ( Clsd ‘ 𝐽 ) → 𝑇 ⊆ ∪ 𝐽 ) |
20 |
18 19
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ⊆ ∪ 𝐽 ) |
21 |
20 14
|
sseqtrrd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝑇 ⊆ 𝑋 ) |
22 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐵 ∈ 𝑇 ) |
23 |
21 22
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐵 ∈ 𝑋 ) |
24 |
17 23
|
ffvelrnd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ) |
25 |
|
eliccxr |
⊢ ( ( 𝐹 ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) |
26 |
24 25
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) |
27 |
|
ifcl |
⊢ ( ( 1 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ* ) |
28 |
7 26 27
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ∈ ℝ* ) |
29 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑆 ) |
30 |
15 29
|
sseldd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → 𝐴 ∈ 𝑋 ) |
31 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
32 |
8 30 23 31
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
33 |
|
xrmin2 |
⊢ ( ( 1 ∈ ℝ* ∧ ( 𝐹 ‘ 𝐵 ) ∈ ℝ* ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ) |
34 |
7 26 33
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐹 ‘ 𝐵 ) ) |
35 |
1
|
metdstri |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) ) |
36 |
8 15 23 30 35
|
syl22anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) ) |
37 |
|
xmetsym |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) ) |
38 |
8 23 30 37
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) ) |
39 |
1
|
metds0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
40 |
8 15 29 39
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
41 |
38 40
|
oveq12d |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) ) |
42 |
32
|
xaddid1d |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) ) |
43 |
41 42
|
eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) ) |
44 |
36 43
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) ) |
45 |
28 26 32 34 44
|
xrletrd |
⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑇 ) ) → if ( 1 ≤ ( 𝐹 ‘ 𝐵 ) , 1 , ( 𝐹 ‘ 𝐵 ) ) ≤ ( 𝐴 𝐷 𝐵 ) ) |