Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) ) |
2 |
|
oveq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐷 𝑦 ) = ( 𝐴 𝐷 𝑦 ) ) |
3 |
2
|
mpteq2dv |
⊢ ( 𝑥 = 𝐴 → ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) ) |
4 |
3
|
rneqd |
⊢ ( 𝑥 = 𝐴 → ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) = ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) ) |
5 |
4
|
infeq1d |
⊢ ( 𝑥 = 𝐴 → inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) = inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ) |
6 |
|
xrltso |
⊢ < Or ℝ* |
7 |
6
|
infex |
⊢ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ∈ V |
8 |
5 1 7
|
fvmpt |
⊢ ( 𝐴 ∈ 𝑋 → ( 𝐹 ‘ 𝐴 ) = inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝐴 𝐷 𝑦 ) ) , ℝ* , < ) ) |