Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
|- ( y = w -> ( x <_ y <-> x <_ w ) ) |
2 |
1
|
rspcv |
|- ( w e. S -> ( A. y e. S x <_ y -> x <_ w ) ) |
3 |
|
breq2 |
|- ( y = x -> ( w <_ y <-> w <_ x ) ) |
4 |
3
|
rspcv |
|- ( x e. S -> ( A. y e. S w <_ y -> w <_ x ) ) |
5 |
2 4
|
im2anan9r |
|- ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> ( x <_ w /\ w <_ x ) ) ) |
6 |
|
ssel |
|- ( S C_ RR -> ( x e. S -> x e. RR ) ) |
7 |
|
ssel |
|- ( S C_ RR -> ( w e. S -> w e. RR ) ) |
8 |
6 7
|
anim12d |
|- ( S C_ RR -> ( ( x e. S /\ w e. S ) -> ( x e. RR /\ w e. RR ) ) ) |
9 |
8
|
impcom |
|- ( ( ( x e. S /\ w e. S ) /\ S C_ RR ) -> ( x e. RR /\ w e. RR ) ) |
10 |
|
letri3 |
|- ( ( x e. RR /\ w e. RR ) -> ( x = w <-> ( x <_ w /\ w <_ x ) ) ) |
11 |
9 10
|
syl |
|- ( ( ( x e. S /\ w e. S ) /\ S C_ RR ) -> ( x = w <-> ( x <_ w /\ w <_ x ) ) ) |
12 |
11
|
exbiri |
|- ( ( x e. S /\ w e. S ) -> ( S C_ RR -> ( ( x <_ w /\ w <_ x ) -> x = w ) ) ) |
13 |
12
|
com23 |
|- ( ( x e. S /\ w e. S ) -> ( ( x <_ w /\ w <_ x ) -> ( S C_ RR -> x = w ) ) ) |
14 |
5 13
|
syld |
|- ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> ( S C_ RR -> x = w ) ) ) |
15 |
14
|
com3r |
|- ( S C_ RR -> ( ( x e. S /\ w e. S ) -> ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) ) |
16 |
15
|
ralrimivv |
|- ( S C_ RR -> A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) |
17 |
16
|
anim1ci |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> ( E. x e. S A. y e. S x <_ y /\ A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) ) |
18 |
|
breq1 |
|- ( x = w -> ( x <_ y <-> w <_ y ) ) |
19 |
18
|
ralbidv |
|- ( x = w -> ( A. y e. S x <_ y <-> A. y e. S w <_ y ) ) |
20 |
19
|
reu4 |
|- ( E! x e. S A. y e. S x <_ y <-> ( E. x e. S A. y e. S x <_ y /\ A. x e. S A. w e. S ( ( A. y e. S x <_ y /\ A. y e. S w <_ y ) -> x = w ) ) ) |
21 |
17 20
|
sylibr |
|- ( ( S C_ RR /\ E. x e. S A. y e. S x <_ y ) -> E! x e. S A. y e. S x <_ y ) |