Metamath Proof Explorer

Theorem xrinfmss

Description: Any subset of extended reals has an infimum. (Contributed by NM, 25-Oct-2005)

Ref Expression
Assertion xrinfmss 
|- ( 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 ) ) )

Proof

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 ) ) )