Metamath Proof Explorer

Theorem ltrelxr

Description: "Less than" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion ltrelxr 
|- < C_ ( RR* X. RR* )

Proof

Step Hyp Ref Expression
1 df-ltxr 
 |-  < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x
2 df-3an 
 |-  ( ( x e. RR /\ y e. RR /\ x  ( ( x e. RR /\ y e. RR ) /\ x
3 2 opabbii 
 |-  { <. x , y >. | ( x e. RR /\ y e. RR /\ x . | ( ( x e. RR /\ y e. RR ) /\ x
4 opabssxp 
 |-  { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ x
5 3 4 eqsstri 
 |-  { <. x , y >. | ( x e. RR /\ y e. RR /\ x
6 rexpssxrxp 
 |-  ( RR X. RR ) C_ ( RR* X. RR* )
7 5 6 sstri 
 |-  { <. x , y >. | ( x e. RR /\ y e. RR /\ x
8 ressxr 
 |-  RR C_ RR*
9 snsspr2 
 |-  { -oo } C_ { +oo , -oo }
10 ssun2 
 |-  { +oo , -oo } C_ ( RR u. { +oo , -oo } )
11 df-xr 
 |-  RR* = ( RR u. { +oo , -oo } )
12 10 11 sseqtrri 
 |-  { +oo , -oo } C_ RR*
13 9 12 sstri 
 |-  { -oo } C_ RR*
14 8 13 unssi 
 |-  ( RR u. { -oo } ) C_ RR*
15 snsspr1 
 |-  { +oo } C_ { +oo , -oo }
16 15 12 sstri 
 |-  { +oo } C_ RR*
17 xpss12 
 |-  ( ( ( RR u. { -oo } ) C_ RR* /\ { +oo } C_ RR* ) -> ( ( RR u. { -oo } ) X. { +oo } ) C_ ( RR* X. RR* ) )
18 14 16 17 mp2an 
 |-  ( ( RR u. { -oo } ) X. { +oo } ) C_ ( RR* X. RR* )
19 xpss12 
 |-  ( ( { -oo } C_ RR* /\ RR C_ RR* ) -> ( { -oo } X. RR ) C_ ( RR* X. RR* ) )
20 13 8 19 mp2an 
 |-  ( { -oo } X. RR ) C_ ( RR* X. RR* )
21 18 20 unssi 
 |-  ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) C_ ( RR* X. RR* )
22 7 21 unssi 
 |-  ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x
23 1 22 eqsstri 
 |-  < C_ ( RR* X. RR* )