This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( 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 bitrid 
 |-  ( ( 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 bitrid 
 |-  ( ( 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 bitrid 
 |-  ( ( 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