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