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 B A < B A < B

Proof

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