Metamath Proof Explorer

Theorem ltxrlt

Description: The standard less-than and the extended real less-than < are identical when restricted to the non-extended reals RR . (Contributed by NM, 13-Oct-2005) (Revised by Mario Carneiro, 28-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 brun 
 |-  ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B <-> ( A ( ( RR u. { -oo } ) X. { +oo } ) B \/ A ( { -oo } X. RR ) B ) )
2 brxp 
 |-  ( A ( ( RR u. { -oo } ) X. { +oo } ) B <-> ( A e. ( RR u. { -oo } ) /\ B e. { +oo } ) )
3 elsni 
 |-  ( B e. { +oo } -> B = +oo )
4 pnfnre 
 |-  +oo e/ RR
5 4 neli 
 |-  -. +oo e. RR
6 simpr 
 |-  ( ( A e. RR /\ B e. RR ) -> B e. RR )
7 eleq1 
 |-  ( B = +oo -> ( B e. RR <-> +oo e. RR ) )
8 6 7 syl5ib 
 |-  ( B = +oo -> ( ( A e. RR /\ B e. RR ) -> +oo e. RR ) )
9 5 8 mtoi 
 |-  ( B = +oo -> -. ( A e. RR /\ B e. RR ) )
10 3 9 syl 
 |-  ( B e. { +oo } -> -. ( A e. RR /\ B e. RR ) )
11 2 10 simplbiim 
 |-  ( A ( ( RR u. { -oo } ) X. { +oo } ) B -> -. ( A e. RR /\ B e. RR ) )
12 brxp 
 |-  ( A ( { -oo } X. RR ) B <-> ( A e. { -oo } /\ B e. RR ) )
13 elsni 
 |-  ( A e. { -oo } -> A = -oo )
14 mnfnre 
 |-  -oo e/ RR
15 14 neli 
 |-  -. -oo e. RR
16 simpl 
 |-  ( ( A e. RR /\ B e. RR ) -> A e. RR )
17 eleq1 
 |-  ( A = -oo -> ( A e. RR <-> -oo e. RR ) )
18 16 17 syl5ib 
 |-  ( A = -oo -> ( ( A e. RR /\ B e. RR ) -> -oo e. RR ) )
19 15 18 mtoi 
 |-  ( A = -oo -> -. ( A e. RR /\ B e. RR ) )
20 13 19 syl 
 |-  ( A e. { -oo } -> -. ( A e. RR /\ B e. RR ) )
21 20 adantr 
 |-  ( ( A e. { -oo } /\ B e. RR ) -> -. ( A e. RR /\ B e. RR ) )
22 12 21 sylbi 
 |-  ( A ( { -oo } X. RR ) B -> -. ( A e. RR /\ B e. RR ) )
23 11 22 jaoi 
 |-  ( ( A ( ( RR u. { -oo } ) X. { +oo } ) B \/ A ( { -oo } X. RR ) B ) -> -. ( A e. RR /\ B e. RR ) )
24 1 23 sylbi 
 |-  ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> -. ( A e. RR /\ B e. RR ) )
25 24 con2i 
 |-  ( ( A e. RR /\ B e. RR ) -> -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B )
26 df-ltxr 
 |-  < = ( { <. x , y >. | ( x e. RR /\ y e. RR /\ x
27 26 equncomi 
 |-  < = ( ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) u. { <. x , y >. | ( x e. RR /\ y e. RR /\ x
28 27 breqi 
 |-  ( A < B <-> A ( ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) u. { <. x , y >. | ( x e. RR /\ y e. RR /\ x
29 brun 
 |-  ( A ( ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) u. { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B \/ A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
30 df-or 
 |-  ( ( A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B \/ A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
31 28 29 30 3bitri 
 |-  ( A < B <-> ( -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
32 biimt 
 |-  ( -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
33 31 32 bitr4id 
 |-  ( -. A ( ( ( RR u. { -oo } ) X. { +oo } ) u. ( { -oo } X. RR ) ) B -> ( A < B <-> A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
34 25 33 syl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
35 breq12 
 |-  ( ( x = A /\ y = B ) -> ( x  A
36 df-3an 
 |-  ( ( x e. RR /\ y e. RR /\ x  ( ( x e. RR /\ y e. RR ) /\ x
37 36 opabbii 
 |-  { <. x , y >. | ( x e. RR /\ y e. RR /\ x . | ( ( x e. RR /\ y e. RR ) /\ x
38 35 37 brab2a 
 |-  ( A { <. x , y >. | ( x e. RR /\ y e. RR /\ x  ( ( A e. RR /\ B e. RR ) /\ A
39 38 baibr 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A  A { <. x , y >. | ( x e. RR /\ y e. RR /\ x
40 34 39 bitr4d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A