Step |
Hyp |
Ref |
Expression |
1 |
|
rnmptlb.1 |
|- ( ph -> E. y e. RR A. x e. A y <_ B ) |
2 |
|
eqid |
|- ( x e. A |-> B ) = ( x e. A |-> B ) |
3 |
2
|
elrnmpt |
|- ( z e. _V -> ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) ) |
4 |
3
|
elv |
|- ( z e. ran ( x e. A |-> B ) <-> E. x e. A z = B ) |
5 |
|
nfra1 |
|- F/ x A. x e. A w <_ B |
6 |
|
nfv |
|- F/ x w <_ z |
7 |
|
rspa |
|- ( ( A. x e. A w <_ B /\ x e. A ) -> w <_ B ) |
8 |
7
|
3adant3 |
|- ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> w <_ B ) |
9 |
|
simp3 |
|- ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> z = B ) |
10 |
8 9
|
breqtrrd |
|- ( ( A. x e. A w <_ B /\ x e. A /\ z = B ) -> w <_ z ) |
11 |
10
|
3exp |
|- ( A. x e. A w <_ B -> ( x e. A -> ( z = B -> w <_ z ) ) ) |
12 |
5 6 11
|
rexlimd |
|- ( A. x e. A w <_ B -> ( E. x e. A z = B -> w <_ z ) ) |
13 |
12
|
imp |
|- ( ( A. x e. A w <_ B /\ E. x e. A z = B ) -> w <_ z ) |
14 |
13
|
adantll |
|- ( ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) /\ E. x e. A z = B ) -> w <_ z ) |
15 |
4 14
|
sylan2b |
|- ( ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) /\ z e. ran ( x e. A |-> B ) ) -> w <_ z ) |
16 |
15
|
ralrimiva |
|- ( ( ( ph /\ w e. RR ) /\ A. x e. A w <_ B ) -> A. z e. ran ( x e. A |-> B ) w <_ z ) |
17 |
|
breq1 |
|- ( y = w -> ( y <_ B <-> w <_ B ) ) |
18 |
17
|
ralbidv |
|- ( y = w -> ( A. x e. A y <_ B <-> A. x e. A w <_ B ) ) |
19 |
18
|
cbvrexvw |
|- ( E. y e. RR A. x e. A y <_ B <-> E. w e. RR A. x e. A w <_ B ) |
20 |
1 19
|
sylib |
|- ( ph -> E. w e. RR A. x e. A w <_ B ) |
21 |
16 20
|
reximddv3 |
|- ( ph -> E. w e. RR A. z e. ran ( x e. A |-> B ) w <_ z ) |
22 |
|
breq1 |
|- ( w = y -> ( w <_ z <-> y <_ z ) ) |
23 |
22
|
ralbidv |
|- ( w = y -> ( A. z e. ran ( x e. A |-> B ) w <_ z <-> A. z e. ran ( x e. A |-> B ) y <_ z ) ) |
24 |
23
|
cbvrexvw |
|- ( E. w e. RR A. z e. ran ( x e. A |-> B ) w <_ z <-> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) |
25 |
21 24
|
sylib |
|- ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) y <_ z ) |