Step |
Hyp |
Ref |
Expression |
1 |
|
rnmptbdd.x |
|- F/ x ph |
2 |
|
rnmptbdd.b |
|- ( ph -> E. y e. RR A. x e. A B <_ y ) |
3 |
|
breq2 |
|- ( y = v -> ( B <_ y <-> B <_ v ) ) |
4 |
3
|
ralbidv |
|- ( y = v -> ( A. x e. A B <_ y <-> A. x e. A B <_ v ) ) |
5 |
4
|
cbvrexvw |
|- ( E. y e. RR A. x e. A B <_ y <-> E. v e. RR A. x e. A B <_ v ) |
6 |
2 5
|
sylib |
|- ( ph -> E. v e. RR A. x e. A B <_ v ) |
7 |
1 6
|
rnmptbddlem |
|- ( ph -> E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v ) |
8 |
|
breq2 |
|- ( v = y -> ( w <_ v <-> w <_ y ) ) |
9 |
8
|
ralbidv |
|- ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. w e. ran ( x e. A |-> B ) w <_ y ) ) |
10 |
|
breq1 |
|- ( w = z -> ( w <_ y <-> z <_ y ) ) |
11 |
10
|
cbvralvw |
|- ( A. w e. ran ( x e. A |-> B ) w <_ y <-> A. z e. ran ( x e. A |-> B ) z <_ y ) |
12 |
9 11
|
bitrdi |
|- ( v = y -> ( A. w e. ran ( x e. A |-> B ) w <_ v <-> A. z e. ran ( x e. A |-> B ) z <_ y ) ) |
13 |
12
|
cbvrexvw |
|- ( E. v e. RR A. w e. ran ( x e. A |-> B ) w <_ v <-> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) |
14 |
7 13
|
sylib |
|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) |