Step |
Hyp |
Ref |
Expression |
1 |
|
0re |
|- 0 e. RR |
2 |
|
rzal |
|- ( A = (/) -> A. y e. A y <_ 0 ) |
3 |
|
brralrspcev |
|- ( ( 0 e. RR /\ A. y e. A y <_ 0 ) -> E. x e. RR A. y e. A y <_ x ) |
4 |
1 2 3
|
sylancr |
|- ( A = (/) -> E. x e. RR A. y e. A y <_ x ) |
5 |
4
|
a1i |
|- ( ( A C_ RR /\ A e. Fin ) -> ( A = (/) -> E. x e. RR A. y e. A y <_ x ) ) |
6 |
|
fimaxre |
|- ( ( A C_ RR /\ A e. Fin /\ A =/= (/) ) -> E. x e. A A. y e. A y <_ x ) |
7 |
6
|
3expia |
|- ( ( A C_ RR /\ A e. Fin ) -> ( A =/= (/) -> E. x e. A A. y e. A y <_ x ) ) |
8 |
|
ssrexv |
|- ( A C_ RR -> ( E. x e. A A. y e. A y <_ x -> E. x e. RR A. y e. A y <_ x ) ) |
9 |
8
|
adantr |
|- ( ( A C_ RR /\ A e. Fin ) -> ( E. x e. A A. y e. A y <_ x -> E. x e. RR A. y e. A y <_ x ) ) |
10 |
7 9
|
syld |
|- ( ( A C_ RR /\ A e. Fin ) -> ( A =/= (/) -> E. x e. RR A. y e. A y <_ x ) ) |
11 |
5 10
|
pm2.61dne |
|- ( ( A C_ RR /\ A e. Fin ) -> E. x e. RR A. y e. A y <_ x ) |