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