Step |
Hyp |
Ref |
Expression |
1 |
|
0red |
|- ( A = (/) -> 0 e. RR ) |
2 |
|
rzal |
|- ( A = (/) -> A. y e. A 0 <_ y ) |
3 |
|
breq1 |
|- ( x = 0 -> ( x <_ y <-> 0 <_ y ) ) |
4 |
3
|
ralbidv |
|- ( x = 0 -> ( A. y e. A x <_ y <-> A. y e. A 0 <_ y ) ) |
5 |
4
|
rspcev |
|- ( ( 0 e. RR /\ A. y e. A 0 <_ y ) -> E. x e. RR A. y e. A x <_ y ) |
6 |
1 2 5
|
syl2anc |
|- ( A = (/) -> E. x e. RR A. y e. A x <_ y ) |
7 |
6
|
adantl |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A = (/) ) -> E. x e. RR A. y e. A x <_ y ) |
8 |
|
neqne |
|- ( -. A = (/) -> A =/= (/) ) |
9 |
8
|
adantl |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ -. A = (/) ) -> A =/= (/) ) |
10 |
|
simpll |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A C_ RR ) |
11 |
|
simplr |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A e. Fin ) |
12 |
|
simpr |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> A =/= (/) ) |
13 |
|
fiminre |
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y ) |
14 |
10 11 12 13
|
syl3anc |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> E. x e. A A. y e. A x <_ y ) |
15 |
|
ssrexv |
|- ( A C_ RR -> ( E. x e. A A. y e. A x <_ y -> E. x e. RR A. y e. A x <_ y ) ) |
16 |
10 14 15
|
sylc |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ A =/= (/) ) -> E. x e. RR A. y e. A x <_ y ) |
17 |
9 16
|
syldan |
|- ( ( ( A C_ RR /\ A e. Fin ) /\ -. A = (/) ) -> E. x e. RR A. y e. A x <_ y ) |
18 |
7 17
|
pm2.61dan |
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A x <_ y ) |