Step |
Hyp |
Ref |
Expression |
1 |
|
r19.29 |
|- ( ( A. y e. A B e. RR /\ E. y e. A z = B ) -> E. y e. A ( B e. RR /\ z = B ) ) |
2 |
|
eleq1 |
|- ( z = B -> ( z e. RR <-> B e. RR ) ) |
3 |
2
|
biimparc |
|- ( ( B e. RR /\ z = B ) -> z e. RR ) |
4 |
3
|
rexlimivw |
|- ( E. y e. A ( B e. RR /\ z = B ) -> z e. RR ) |
5 |
1 4
|
syl |
|- ( ( A. y e. A B e. RR /\ E. y e. A z = B ) -> z e. RR ) |
6 |
5
|
ex |
|- ( A. y e. A B e. RR -> ( E. y e. A z = B -> z e. RR ) ) |
7 |
6
|
abssdv |
|- ( A. y e. A B e. RR -> { z | E. y e. A z = B } C_ RR ) |
8 |
|
abrexfi |
|- ( A e. Fin -> { z | E. y e. A z = B } e. Fin ) |
9 |
|
fimaxre2 |
|- ( ( { z | E. y e. A z = B } C_ RR /\ { z | E. y e. A z = B } e. Fin ) -> E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x ) |
10 |
7 8 9
|
syl2anr |
|- ( ( A e. Fin /\ A. y e. A B e. RR ) -> E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x ) |
11 |
|
r19.23v |
|- ( A. y e. A ( w = B -> w <_ x ) <-> ( E. y e. A w = B -> w <_ x ) ) |
12 |
11
|
albii |
|- ( A. w A. y e. A ( w = B -> w <_ x ) <-> A. w ( E. y e. A w = B -> w <_ x ) ) |
13 |
|
ralcom4 |
|- ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. w A. y e. A ( w = B -> w <_ x ) ) |
14 |
|
eqeq1 |
|- ( z = w -> ( z = B <-> w = B ) ) |
15 |
14
|
rexbidv |
|- ( z = w -> ( E. y e. A z = B <-> E. y e. A w = B ) ) |
16 |
15
|
ralab |
|- ( A. w e. { z | E. y e. A z = B } w <_ x <-> A. w ( E. y e. A w = B -> w <_ x ) ) |
17 |
12 13 16
|
3bitr4i |
|- ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. w e. { z | E. y e. A z = B } w <_ x ) |
18 |
|
nfv |
|- F/ w B <_ x |
19 |
|
breq1 |
|- ( w = B -> ( w <_ x <-> B <_ x ) ) |
20 |
18 19
|
ceqsalg |
|- ( B e. RR -> ( A. w ( w = B -> w <_ x ) <-> B <_ x ) ) |
21 |
20
|
ralimi |
|- ( A. y e. A B e. RR -> A. y e. A ( A. w ( w = B -> w <_ x ) <-> B <_ x ) ) |
22 |
|
ralbi |
|- ( A. y e. A ( A. w ( w = B -> w <_ x ) <-> B <_ x ) -> ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. y e. A B <_ x ) ) |
23 |
21 22
|
syl |
|- ( A. y e. A B e. RR -> ( A. y e. A A. w ( w = B -> w <_ x ) <-> A. y e. A B <_ x ) ) |
24 |
17 23
|
bitr3id |
|- ( A. y e. A B e. RR -> ( A. w e. { z | E. y e. A z = B } w <_ x <-> A. y e. A B <_ x ) ) |
25 |
24
|
rexbidv |
|- ( A. y e. A B e. RR -> ( E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x <-> E. x e. RR A. y e. A B <_ x ) ) |
26 |
25
|
adantl |
|- ( ( A e. Fin /\ A. y e. A B e. RR ) -> ( E. x e. RR A. w e. { z | E. y e. A z = B } w <_ x <-> E. x e. RR A. y e. A B <_ x ) ) |
27 |
10 26
|
mpbid |
|- ( ( A e. Fin /\ A. y e. A B e. RR ) -> E. x e. RR A. y e. A B <_ x ) |