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