Step |
Hyp |
Ref |
Expression |
1 |
|
infxrlb |
|- ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) <_ -oo ) |
2 |
|
infxrcl |
|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* ) |
3 |
2
|
adantr |
|- ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) e. RR* ) |
4 |
|
xlemnf |
|- ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) <_ -oo <-> inf ( A , RR* , < ) = -oo ) ) |
5 |
3 4
|
syl |
|- ( ( A C_ RR* /\ -oo e. A ) -> ( inf ( A , RR* , < ) <_ -oo <-> inf ( A , RR* , < ) = -oo ) ) |
6 |
1 5
|
mpbid |
|- ( ( A C_ RR* /\ -oo e. A ) -> inf ( A , RR* , < ) = -oo ) |