Step |
Hyp |
Ref |
Expression |
1 |
|
suprubrnmpt2.x |
|- F/ x ph |
2 |
|
suprubrnmpt2.b |
|- ( ( ph /\ x e. A ) -> B e. RR ) |
3 |
|
suprubrnmpt2.l |
|- ( ph -> E. y e. RR A. x e. A B <_ y ) |
4 |
|
suprubrnmpt2.c |
|- ( ph -> C e. A ) |
5 |
|
suprubrnmpt2.d |
|- ( ph -> D e. RR ) |
6 |
|
suprubrnmpt2.i |
|- ( x = C -> B = D ) |
7 |
|
eqid |
|- ( x e. A |-> B ) = ( x e. A |-> B ) |
8 |
1 7 2
|
rnmptssd |
|- ( ph -> ran ( x e. A |-> B ) C_ RR ) |
9 |
7 6
|
elrnmpt1s |
|- ( ( C e. A /\ D e. RR ) -> D e. ran ( x e. A |-> B ) ) |
10 |
4 5 9
|
syl2anc |
|- ( ph -> D e. ran ( x e. A |-> B ) ) |
11 |
10
|
ne0d |
|- ( ph -> ran ( x e. A |-> B ) =/= (/) ) |
12 |
1 3
|
rnmptbdd |
|- ( ph -> E. y e. RR A. w e. ran ( x e. A |-> B ) w <_ y ) |
13 |
8 11 12 10
|
suprubd |
|- ( ph -> D <_ sup ( ran ( x e. A |-> B ) , RR , < ) ) |