Step |
Hyp |
Ref |
Expression |
1 |
|
metdscn.f |
|- F = ( x e. X |-> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) ) |
2 |
|
oveq1 |
|- ( x = A -> ( x D y ) = ( A D y ) ) |
3 |
2
|
mpteq2dv |
|- ( x = A -> ( y e. S |-> ( x D y ) ) = ( y e. S |-> ( A D y ) ) ) |
4 |
3
|
rneqd |
|- ( x = A -> ran ( y e. S |-> ( x D y ) ) = ran ( y e. S |-> ( A D y ) ) ) |
5 |
4
|
infeq1d |
|- ( x = A -> inf ( ran ( y e. S |-> ( x D y ) ) , RR* , < ) = inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) ) |
6 |
|
xrltso |
|- < Or RR* |
7 |
6
|
infex |
|- inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) e. _V |
8 |
5 1 7
|
fvmpt |
|- ( A e. X -> ( F ` A ) = inf ( ran ( y e. S |-> ( A D y ) ) , RR* , < ) ) |