Metamath Proof Explorer


Theorem ltxr

Description: The 'less than' binary relation on the set of extended reals. Definition 12-3.1 of Gleason p. 173. (Contributed by NM, 14-Oct-2005)

Ref Expression
Assertion ltxr
|- ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> ( ( ( ( A e. RR /\ B e. RR ) /\ A 

Proof

Step Hyp Ref Expression
1 breq12
 |-  ( ( x = A /\ y = B ) -> ( x  A 
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 1 3 brab2a
 |-  ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( ( A e. RR /\ B e. RR ) /\ A 
5 4 a1i
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( ( A e. RR /\ B e. RR ) /\ A 
6 brun
 |-  ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B <-> ( A ( ( RR u. { -oo } ) X. { +oo } ) B \/ A ( { -oo } X. RR ) B ) )
7 brxp
 |-  ( A ( ( RR u. { -oo } ) X. { +oo } ) B <-> ( A e. ( RR u. { -oo } ) /\ B e. { +oo } ) )
8 elun
 |-  ( A e. ( RR u. { -oo } ) <-> ( A e. RR \/ A e. { -oo } ) )
9 orcom
 |-  ( ( A e. RR \/ A e. { -oo } ) <-> ( A e. { -oo } \/ A e. RR ) )
10 8 9 bitri
 |-  ( A e. ( RR u. { -oo } ) <-> ( A e. { -oo } \/ A e. RR ) )
11 elsng
 |-  ( A e. RR* -> ( A e. { -oo } <-> A = -oo ) )
12 11 orbi1d
 |-  ( A e. RR* -> ( ( A e. { -oo } \/ A e. RR ) <-> ( A = -oo \/ A e. RR ) ) )
13 10 12 syl5bb
 |-  ( A e. RR* -> ( A e. ( RR u. { -oo } ) <-> ( A = -oo \/ A e. RR ) ) )
14 elsng
 |-  ( B e. RR* -> ( B e. { +oo } <-> B = +oo ) )
15 13 14 bi2anan9
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A e. ( RR u. { -oo } ) /\ B e. { +oo } ) <-> ( ( A = -oo \/ A e. RR ) /\ B = +oo ) ) )
16 andir
 |-  ( ( ( A = -oo \/ A e. RR ) /\ B = +oo ) <-> ( ( A = -oo /\ B = +oo ) \/ ( A e. RR /\ B = +oo ) ) )
17 15 16 bitrdi
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A e. ( RR u. { -oo } ) /\ B e. { +oo } ) <-> ( ( A = -oo /\ B = +oo ) \/ ( A e. RR /\ B = +oo ) ) ) )
18 7 17 syl5bb
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A ( ( RR u. { -oo } ) X. { +oo } ) B <-> ( ( A = -oo /\ B = +oo ) \/ ( A e. RR /\ B = +oo ) ) ) )
19 brxp
 |-  ( A ( { -oo } X. RR ) B <-> ( A e. { -oo } /\ B e. RR ) )
20 11 anbi1d
 |-  ( A e. RR* -> ( ( A e. { -oo } /\ B e. RR ) <-> ( A = -oo /\ B e. RR ) ) )
21 20 adantr
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A e. { -oo } /\ B e. RR ) <-> ( A = -oo /\ B e. RR ) ) )
22 19 21 syl5bb
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A ( { -oo } X. RR ) B <-> ( A = -oo /\ B e. RR ) ) )
23 18 22 orbi12d
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A ( ( RR u. { -oo } ) X. { +oo } ) B \/ A ( { -oo } X. RR ) B ) <-> ( ( ( A = -oo /\ B = +oo ) \/ ( A e. RR /\ B = +oo ) ) \/ ( A = -oo /\ B e. RR ) ) ) )
24 orass
 |-  ( ( ( ( A = -oo /\ B = +oo ) \/ ( A e. RR /\ B = +oo ) ) \/ ( A = -oo /\ B e. RR ) ) <-> ( ( A = -oo /\ B = +oo ) \/ ( ( A e. RR /\ B = +oo ) \/ ( A = -oo /\ B e. RR ) ) ) )
25 23 24 bitrdi
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A ( ( RR u. { -oo } ) X. { +oo } ) B \/ A ( { -oo } X. RR ) B ) <-> ( ( A = -oo /\ B = +oo ) \/ ( ( A e. RR /\ B = +oo ) \/ ( A = -oo /\ B e. RR ) ) ) ) )
26 6 25 syl5bb
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B <-> ( ( A = -oo /\ B = +oo ) \/ ( ( A e. RR /\ B = +oo ) \/ ( A = -oo /\ B e. RR ) ) ) ) )
27 5 26 orbi12d
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( ( ( A e. RR /\ B e. RR ) /\ A 
28 df-ltxr
 |-  < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x 
29 28 breqi
 |-  ( A < B <-> A ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x 
30 brun
 |-  ( A ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x 
31 29 30 bitri
 |-  ( A < B <-> ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x 
32 orass
 |-  ( ( ( ( ( A e. RR /\ B e. RR ) /\ A  ( ( ( A e. RR /\ B e. RR ) /\ A 
33 27 31 32 3bitr4g
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < B <-> ( ( ( ( A e. RR /\ B e. RR ) /\ A