Step |
Hyp |
Ref |
Expression |
1 |
|
ralnex |
|- ( A. x e. RR -. A. y e. A x <_ y <-> -. E. x e. RR A. y e. A x <_ y ) |
2 |
|
ssel2 |
|- ( ( A C_ RR* /\ y e. A ) -> y e. RR* ) |
3 |
|
rexr |
|- ( x e. RR -> x e. RR* ) |
4 |
|
simpl |
|- ( ( y e. RR* /\ x e. RR* ) -> y e. RR* ) |
5 |
|
simpr |
|- ( ( y e. RR* /\ x e. RR* ) -> x e. RR* ) |
6 |
4 5
|
xrltnled |
|- ( ( y e. RR* /\ x e. RR* ) -> ( y < x <-> -. x <_ y ) ) |
7 |
2 3 6
|
syl2an |
|- ( ( ( A C_ RR* /\ y e. A ) /\ x e. RR ) -> ( y < x <-> -. x <_ y ) ) |
8 |
7
|
an32s |
|- ( ( ( A C_ RR* /\ x e. RR ) /\ y e. A ) -> ( y < x <-> -. x <_ y ) ) |
9 |
8
|
rexbidva |
|- ( ( A C_ RR* /\ x e. RR ) -> ( E. y e. A y < x <-> E. y e. A -. x <_ y ) ) |
10 |
|
rexnal |
|- ( E. y e. A -. x <_ y <-> -. A. y e. A x <_ y ) |
11 |
9 10
|
bitr2di |
|- ( ( A C_ RR* /\ x e. RR ) -> ( -. A. y e. A x <_ y <-> E. y e. A y < x ) ) |
12 |
11
|
ralbidva |
|- ( A C_ RR* -> ( A. x e. RR -. A. y e. A x <_ y <-> A. x e. RR E. y e. A y < x ) ) |
13 |
1 12
|
bitr3id |
|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A x <_ y <-> A. x e. RR E. y e. A y < x ) ) |
14 |
|
infxrunb2 |
|- ( A C_ RR* -> ( A. x e. RR E. y e. A y < x <-> inf ( A , RR* , < ) = -oo ) ) |
15 |
|
infxrcl |
|- ( A C_ RR* -> inf ( A , RR* , < ) e. RR* ) |
16 |
|
ngtmnft |
|- ( inf ( A , RR* , < ) e. RR* -> ( inf ( A , RR* , < ) = -oo <-> -. -oo < inf ( A , RR* , < ) ) ) |
17 |
15 16
|
syl |
|- ( A C_ RR* -> ( inf ( A , RR* , < ) = -oo <-> -. -oo < inf ( A , RR* , < ) ) ) |
18 |
13 14 17
|
3bitrd |
|- ( A C_ RR* -> ( -. E. x e. RR A. y e. A x <_ y <-> -. -oo < inf ( A , RR* , < ) ) ) |
19 |
18
|
con4bid |
|- ( A C_ RR* -> ( E. x e. RR A. y e. A x <_ y <-> -oo < inf ( A , RR* , < ) ) ) |