Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
simprr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 ) |
3 |
|
simpr |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ 𝑋 ) |
4 |
3
|
sselda |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 ) |
5 |
4
|
adantrr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐴 ∈ 𝑋 ) |
6 |
2 5
|
jca |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) |
7 |
1
|
metdstri |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) ) |
8 |
6 7
|
syldan |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) ) |
9 |
|
simpll |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) |
10 |
|
xmetsym |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) ) |
11 |
9 2 5 10
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 𝐷 𝐴 ) = ( 𝐴 𝐷 𝐵 ) ) |
12 |
1
|
metds0 |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
13 |
12
|
3expa |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
14 |
13
|
adantrr |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐴 ) = 0 ) |
15 |
11 14
|
oveq12d |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) ) |
16 |
|
xmetcl |
⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
17 |
9 5 2 16
|
syl3anc |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ ℝ* ) |
18 |
17
|
xaddid1d |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐴 𝐷 𝐵 ) +𝑒 0 ) = ( 𝐴 𝐷 𝐵 ) ) |
19 |
15 18
|
eqtrd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( ( 𝐵 𝐷 𝐴 ) +𝑒 ( 𝐹 ‘ 𝐴 ) ) = ( 𝐴 𝐷 𝐵 ) ) |
20 |
8 19
|
breqtrd |
⊢ ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐹 ‘ 𝐵 ) ≤ ( 𝐴 𝐷 𝐵 ) ) |