Theorem ltxr 8465

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.)

Assertion

Ref	Expression
ltxr	|- ((A e. RR* /\ B e. RR*) -> (A < B <-> ((((A e. RR /\ B e. RR) /\ A <RR B) \/ (A = -oo /\ B = +oo)) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR)))))

Proof of Theorem ltxr

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breq12 3760	. . . . 5 |- ((x = A /\ y = B) -> (x <RR y <-> A <RR B))
2		df-3an 886	. . . . . 6 |- ((x e. RR /\ y e. RR /\ x <RR y) <-> ((x e. RR /\ y e. RR) /\ x <RR y))
3	2	opabbii 3815	. . . . 5 |- { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) } = { <.x , y >. | ((x e. RR /\ y e. RR) /\ x <RR y) }
4	1, 3	brab2ga 4358	. . . 4 |- (A { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) }B <-> ((A e. RR /\ B e. RR) /\ A <RR B))
5	4	a1i 9	. . 3 |- ((A e. RR* /\ B e. RR*) -> (A { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) }B <-> ((A e. RR /\ B e. RR) /\ A <RR B)))
6		brun 3801	. . . 4 |- (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 4318	. . . . . . 7 |- (A(( RR u. { -oo }) X. { +oo })B <-> (A e. ( RR u. { -oo }) /\ B e. { +oo }))
8		elun 3078	. . . . . . . . . . 11 |- (A e. ( RR u. { -oo }) <-> (A e. RR \/ A e. { -oo }))
9		orcom 646	. . . . . . . . . . 11 |- ((A e. RR \/ A e. { -oo }) <-> (A e. { -oo } \/ A e. RR))
10	8, 9	bitri 173	. . . . . . . . . 10 |- (A e. ( RR u. { -oo }) <-> (A e. { -oo } \/ A e. RR))
11		elsncg 3389	. . . . . . . . . . 11 |- (A e. RR* -> (A e. { -oo } <-> A = -oo))
12	11	orbi1d 704	. . . . . . . . . 10 |- (A e. RR* -> ((A e. { -oo } \/ A e. RR) <-> (A = -oo \/ A e. RR)))
13	10, 12	syl5bb 181	. . . . . . . . 9 |- (A e. RR* -> (A e. ( RR u. { -oo }) <-> (A = -oo \/ A e. RR)))
14		elsncg 3389	. . . . . . . . 9 |- (B e. RR* -> (B e. { +oo } <-> B = +oo))
15	13, 14	bi2anan9 538	. . . . . . . 8 |- ((A e. RR* /\ B e. RR*) -> ((A e. ( RR u. { -oo }) /\ B e. { +oo }) <-> ((A = -oo \/ A e. RR) /\ B = +oo)))
16		andir 731	. . . . . . . 8 |- (((A = -oo \/ A e. RR) /\ B = +oo) <-> ((A = -oo /\ B = +oo) \/ (A e. RR /\ B = +oo)))
17	15, 16	syl6bb 185	. . . . . . 7 |- ((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 181	. . . . . 6 |- ((A e. RR* /\ B e. RR*) -> (A(( RR u. { -oo }) X. { +oo })B <-> ((A = -oo /\ B = +oo) \/ (A e. RR /\ B = +oo))))
19		brxp 4318	. . . . . . 7 |- (A( { -oo } X. RR)B <-> (A e. { -oo } /\ B e. RR))
20	11	anbi1d 438	. . . . . . . 8 |- (A e. RR* -> ((A e. { -oo } /\ B e. RR) <-> (A = -oo /\ B e. RR)))
21	20	adantr 261	. . . . . . 7 |- ((A e. RR* /\ B e. RR*) -> ((A e. { -oo } /\ B e. RR) <-> (A = -oo /\ B e. RR)))
22	19, 21	syl5bb 181	. . . . . 6 |- ((A e. RR* /\ B e. RR*) -> (A( { -oo } X. RR)B <-> (A = -oo /\ B e. RR)))
23	18, 22	orbi12d 706	. . . . 5 |- ((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 683	. . . . 5 |- ((((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	syl6bb 185	. . . 4 |- ((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 181	. . 3 |- ((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 706	. 2 |- ((A e. RR* /\ B e. RR*) -> ((A { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) }B \/ A((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR))B) <-> (((A e. RR /\ B e. RR) /\ A <RR B) \/ ((A = -oo /\ B = +oo) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR))))))
28		df-ltxr 6862	. . . 4 |- < = ( { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) } u. ((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR)))
29	28	breqi 3761	. . 3 |- (A < B <-> A( { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) } u. ((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR)))B)
30		brun 3801	. . 3 |- (A( { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) } u. ((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR)))B <-> (A { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) }B \/ A((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR))B))
31	29, 30	bitri 173	. 2 |- (A < B <-> (A { <.x , y >. | (x e. RR /\ y e. RR /\ x <RR y) }B \/ A((( RR u. { -oo }) X. { +oo }) u. ( { -oo } X. RR))B))
32		orass 683	. 2 |- (((((A e. RR /\ B e. RR) /\ A <RR B) \/ (A = -oo /\ B = +oo)) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR))) <-> (((A e. RR /\ B e. RR) /\ A <RR B) \/ ((A = -oo /\ B = +oo) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR)))))
33	27, 31, 32	3bitr4g 212	1 |- ((A e. RR* /\ B e. RR*) -> (A < B <-> ((((A e. RR /\ B e. RR) /\ A <RR B) \/ (A = -oo /\ B = +oo)) \/ ((A e. RR /\ B = +oo) \/ (A = -oo /\ B e. RR)))))

Syntax hints:   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628   /\ w3a 884   = wceq 1242   e. wcel 1390   u. cun 2909   {csn 3367   class class class wbr 3755   {copab 3808   X. cxp 4286   RRcr 6710   <RR cltrr 6715   +oocpnf 6854   -oocmnf 6855   RR*cxr 6856   < clt 6857

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-xp 4294  df-ltxr 6862

This theorem is referenced by:  xrltnr  8471  ltpnf  8472  mnflt  8474  mnfltpnf  8476  pnfnlt  8478  nltmnf  8479