Metamath Proof Explorer

Theorem ssxr

Description: The three (non-exclusive) possibilities implied by a subset of extended reals. (Contributed by NM, 25-Oct-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion ssxr 
|- ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { +oo , -oo } = ( { +oo } u. { -oo } )
2 1 ineq2i 
 |-  ( A i^i { +oo , -oo } ) = ( A i^i ( { +oo } u. { -oo } ) )
3 indi 
 |-  ( A i^i ( { +oo } u. { -oo } ) ) = ( ( A i^i { +oo } ) u. ( A i^i { -oo } ) )
4 2 3 eqtri 
 |-  ( A i^i { +oo , -oo } ) = ( ( A i^i { +oo } ) u. ( A i^i { -oo } ) )
5 disjsn 
 |-  ( ( A i^i { +oo } ) = (/) <-> -. +oo e. A )
6 disjsn 
 |-  ( ( A i^i { -oo } ) = (/) <-> -. -oo e. A )
7 5 6 anbi12i 
 |-  ( ( ( A i^i { +oo } ) = (/) /\ ( A i^i { -oo } ) = (/) ) <-> ( -. +oo e. A /\ -. -oo e. A ) )
8 7 biimpri 
 |-  ( ( -. +oo e. A /\ -. -oo e. A ) -> ( ( A i^i { +oo } ) = (/) /\ ( A i^i { -oo } ) = (/) ) )
9 pm4.56 
 |-  ( ( -. +oo e. A /\ -. -oo e. A ) <-> -. ( +oo e. A \/ -oo e. A ) )
10 un00 
 |-  ( ( ( A i^i { +oo } ) = (/) /\ ( A i^i { -oo } ) = (/) ) <-> ( ( A i^i { +oo } ) u. ( A i^i { -oo } ) ) = (/) )
11 8 9 10 3imtr3i 
 |-  ( -. ( +oo e. A \/ -oo e. A ) -> ( ( A i^i { +oo } ) u. ( A i^i { -oo } ) ) = (/) )
12 4 11 eqtrid 
 |-  ( -. ( +oo e. A \/ -oo e. A ) -> ( A i^i { +oo , -oo } ) = (/) )
13 reldisj 
 |-  ( A C_ ( RR u. { +oo , -oo } ) -> ( ( A i^i { +oo , -oo } ) = (/) <-> A C_ ( ( RR u. { +oo , -oo } ) \ { +oo , -oo } ) ) )
14 renfdisj 
 |-  ( RR i^i { +oo , -oo } ) = (/)
15 disj3 
 |-  ( ( RR i^i { +oo , -oo } ) = (/) <-> RR = ( RR \ { +oo , -oo } ) )
16 14 15 mpbi 
 |-  RR = ( RR \ { +oo , -oo } )
17 difun2 
 |-  ( ( RR u. { +oo , -oo } ) \ { +oo , -oo } ) = ( RR \ { +oo , -oo } )
18 16 17 eqtr4i 
 |-  RR = ( ( RR u. { +oo , -oo } ) \ { +oo , -oo } )
19 18 sseq2i 
 |-  ( A C_ RR <-> A C_ ( ( RR u. { +oo , -oo } ) \ { +oo , -oo } ) )
20 13 19 bitr4di 
 |-  ( A C_ ( RR u. { +oo , -oo } ) -> ( ( A i^i { +oo , -oo } ) = (/) <-> A C_ RR ) )
21 12 20 syl5ib 
 |-  ( A C_ ( RR u. { +oo , -oo } ) -> ( -. ( +oo e. A \/ -oo e. A ) -> A C_ RR ) )
22 21 orrd 
 |-  ( A C_ ( RR u. { +oo , -oo } ) -> ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) )
23 df-xr 
 |-  RR* = ( RR u. { +oo , -oo } )
24 23 sseq2i 
 |-  ( A C_ RR* <-> A C_ ( RR u. { +oo , -oo } ) )
25 3orrot 
 |-  ( ( A C_ RR \/ +oo e. A \/ -oo e. A ) <-> ( +oo e. A \/ -oo e. A \/ A C_ RR ) )
26 df-3or 
 |-  ( ( +oo e. A \/ -oo e. A \/ A C_ RR ) <-> ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) )
27 25 26 bitri 
 |-  ( ( A C_ RR \/ +oo e. A \/ -oo e. A ) <-> ( ( +oo e. A \/ -oo e. A ) \/ A C_ RR ) )
28 22 24 27 3imtr4i 
 |-  ( A C_ RR* -> ( A C_ RR \/ +oo e. A \/ -oo e. A ) )