Step |
Hyp |
Ref |
Expression |
1 |
|
xrinfmsslem |
|- ( ( A C_ RR* /\ ( A C_ RR \/ -oo e. A ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) |
2 |
|
ssdifss |
|- ( A C_ RR* -> ( A \ { +oo } ) C_ RR* ) |
3 |
|
ssxr |
|- ( ( A \ { +oo } ) C_ RR* -> ( ( A \ { +oo } ) C_ RR \/ +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) ) |
4 |
|
3orass |
|- ( ( ( A \ { +oo } ) C_ RR \/ +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) <-> ( ( A \ { +oo } ) C_ RR \/ ( +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) ) ) |
5 |
|
pnfex |
|- +oo e. _V |
6 |
5
|
snid |
|- +oo e. { +oo } |
7 |
|
elndif |
|- ( +oo e. { +oo } -> -. +oo e. ( A \ { +oo } ) ) |
8 |
|
biorf |
|- ( -. +oo e. ( A \ { +oo } ) -> ( -oo e. ( A \ { +oo } ) <-> ( +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) ) ) |
9 |
6 7 8
|
mp2b |
|- ( -oo e. ( A \ { +oo } ) <-> ( +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) ) |
10 |
9
|
orbi2i |
|- ( ( ( A \ { +oo } ) C_ RR \/ -oo e. ( A \ { +oo } ) ) <-> ( ( A \ { +oo } ) C_ RR \/ ( +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) ) ) |
11 |
4 10
|
bitr4i |
|- ( ( ( A \ { +oo } ) C_ RR \/ +oo e. ( A \ { +oo } ) \/ -oo e. ( A \ { +oo } ) ) <-> ( ( A \ { +oo } ) C_ RR \/ -oo e. ( A \ { +oo } ) ) ) |
12 |
3 11
|
sylib |
|- ( ( A \ { +oo } ) C_ RR* -> ( ( A \ { +oo } ) C_ RR \/ -oo e. ( A \ { +oo } ) ) ) |
13 |
|
xrinfmsslem |
|- ( ( ( A \ { +oo } ) C_ RR* /\ ( ( A \ { +oo } ) C_ RR \/ -oo e. ( A \ { +oo } ) ) ) -> E. x e. RR* ( A. y e. ( A \ { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A \ { +oo } ) z < y ) ) ) |
14 |
2 12 13
|
syl2anc2 |
|- ( A C_ RR* -> E. x e. RR* ( A. y e. ( A \ { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A \ { +oo } ) z < y ) ) ) |
15 |
|
xrinfmexpnf |
|- ( E. x e. RR* ( A. y e. ( A \ { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A \ { +oo } ) z < y ) ) -> E. x e. RR* ( A. y e. ( ( A \ { +oo } ) u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) ) ) |
16 |
5
|
snss |
|- ( +oo e. A <-> { +oo } C_ A ) |
17 |
|
undif |
|- ( { +oo } C_ A <-> ( { +oo } u. ( A \ { +oo } ) ) = A ) |
18 |
|
uncom |
|- ( { +oo } u. ( A \ { +oo } ) ) = ( ( A \ { +oo } ) u. { +oo } ) |
19 |
18
|
eqeq1i |
|- ( ( { +oo } u. ( A \ { +oo } ) ) = A <-> ( ( A \ { +oo } ) u. { +oo } ) = A ) |
20 |
17 19
|
bitri |
|- ( { +oo } C_ A <-> ( ( A \ { +oo } ) u. { +oo } ) = A ) |
21 |
16 20
|
bitri |
|- ( +oo e. A <-> ( ( A \ { +oo } ) u. { +oo } ) = A ) |
22 |
|
raleq |
|- ( ( ( A \ { +oo } ) u. { +oo } ) = A -> ( A. y e. ( ( A \ { +oo } ) u. { +oo } ) -. y < x <-> A. y e. A -. y < x ) ) |
23 |
|
rexeq |
|- ( ( ( A \ { +oo } ) u. { +oo } ) = A -> ( E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y <-> E. z e. A z < y ) ) |
24 |
23
|
imbi2d |
|- ( ( ( A \ { +oo } ) u. { +oo } ) = A -> ( ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) <-> ( x < y -> E. z e. A z < y ) ) ) |
25 |
24
|
ralbidv |
|- ( ( ( A \ { +oo } ) u. { +oo } ) = A -> ( A. y e. RR* ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) <-> A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) |
26 |
22 25
|
anbi12d |
|- ( ( ( A \ { +oo } ) u. { +oo } ) = A -> ( ( A. y e. ( ( A \ { +oo } ) u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) ) <-> ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) ) |
27 |
21 26
|
sylbi |
|- ( +oo e. A -> ( ( A. y e. ( ( A \ { +oo } ) u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) ) <-> ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) ) |
28 |
27
|
rexbidv |
|- ( +oo e. A -> ( E. x e. RR* ( A. y e. ( ( A \ { +oo } ) u. { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( ( A \ { +oo } ) u. { +oo } ) z < y ) ) <-> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) ) |
29 |
15 28
|
syl5ib |
|- ( +oo e. A -> ( E. x e. RR* ( A. y e. ( A \ { +oo } ) -. y < x /\ A. y e. RR* ( x < y -> E. z e. ( A \ { +oo } ) z < y ) ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) ) |
30 |
14 29
|
mpan9 |
|- ( ( A C_ RR* /\ +oo e. A ) -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) |
31 |
|
ssxr |
|- ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) ) |
32 |
|
df-3or |
|- ( ( A C_ RR \/ +oo e. A \/ -oo e. A ) <-> ( ( A C_ RR \/ +oo e. A ) \/ -oo e. A ) ) |
33 |
|
or32 |
|- ( ( ( A C_ RR \/ +oo e. A ) \/ -oo e. A ) <-> ( ( A C_ RR \/ -oo e. A ) \/ +oo e. A ) ) |
34 |
32 33
|
bitri |
|- ( ( A C_ RR \/ +oo e. A \/ -oo e. A ) <-> ( ( A C_ RR \/ -oo e. A ) \/ +oo e. A ) ) |
35 |
31 34
|
sylib |
|- ( A C_ RR* -> ( ( A C_ RR \/ -oo e. A ) \/ +oo e. A ) ) |
36 |
1 30 35
|
mpjaodan |
|- ( A C_ RR* -> E. x e. RR* ( A. y e. A -. y < x /\ A. y e. RR* ( x < y -> E. z e. A z < y ) ) ) |