Theorem xrltso 8447

Description: 'Less than' is a weakly linear ordering on the extended reals. (Contributed by NM, 15-Oct-2005.)

Assertion

Ref	Expression
xrltso	|- < Or RR*

Proof of Theorem xrltso

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

Step	Hyp	Ref	Expression
1		xrltnr 8431	. . . . 5 |- (x e. RR* -> -. x < x)
2	1	adantl 262	. . . 4 |- (( T. /\ x e. RR*) -> -. x < x)
3		xrlttr 8446	. . . . 5 |- ((x e. RR* /\ y e. RR* /\ z e. RR*) -> ((x < y /\ y < z) -> x < z))
4	3	adantl 262	. . . 4 |- (( T. /\ (x e. RR* /\ y e. RR* /\ z e. RR*)) -> ((x < y /\ y < z) -> x < z))
5	2, 4	ispod 4032	. . 3 |- ( T. -> < Po RR*)
6	5	trud 1251	. 2 |- < Po RR*
7		elxr 8426	. . . . 5 |- (x e. RR* <-> (x e. RR \/ x = +oo \/ x = -oo))
8		elxr 8426	. . . . . . . . . 10 |- (y e. RR* <-> (y e. RR \/ y = +oo \/ y = -oo))
9		elxr 8426	. . . . . . . . . . . . . 14 |- (z e. RR* <-> (z e. RR \/ z = +oo \/ z = -oo))
10		simplr 482	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ x e. RR) /\ z e. RR) -> x e. RR)
11		simpll 481	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ x e. RR) /\ z e. RR) -> y e. RR)
12		simpr 103	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ x e. RR) /\ z e. RR) -> z e. RR)
13		axltwlin 6844	. . . . . . . . . . . . . . . 16 |- ((x e. RR /\ y e. RR /\ z e. RR) -> (x < y -> (x < z \/ z < y)))
14	10, 11, 12, 13	syl3anc 1134	. . . . . . . . . . . . . . 15 |- (((y e. RR /\ x e. RR) /\ z e. RR) -> (x < y -> (x < z \/ z < y)))
15		ltpnf 8432	. . . . . . . . . . . . . . . . . . 19 |- (x e. RR -> x < +oo)
16	15	ad2antlr 458	. . . . . . . . . . . . . . . . . 18 |- (((y e. RR /\ x e. RR) /\ z = +oo) -> x < +oo)
17		breq2 3759	. . . . . . . . . . . . . . . . . . 19 |- (z = +oo -> (x < z <-> x < +oo))
18	17	adantl 262	. . . . . . . . . . . . . . . . . 18 |- (((y e. RR /\ x e. RR) /\ z = +oo) -> (x < z <-> x < +oo))
19	16, 18	mpbird 156	. . . . . . . . . . . . . . . . 17 |- (((y e. RR /\ x e. RR) /\ z = +oo) -> x < z)
20	19	orcd 651	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ x e. RR) /\ z = +oo) -> (x < z \/ z < y))
21	20	a1d 22	. . . . . . . . . . . . . . 15 |- (((y e. RR /\ x e. RR) /\ z = +oo) -> (x < y -> (x < z \/ z < y)))
22		mnflt 8434	. . . . . . . . . . . . . . . . . . 19 |- (y e. RR -> -oo < y)
23	22	ad2antrr 457	. . . . . . . . . . . . . . . . . 18 |- (((y e. RR /\ x e. RR) /\ z = -oo) -> -oo < y)
24		breq1 3758	. . . . . . . . . . . . . . . . . . 19 |- (z = -oo -> (z < y <-> -oo < y))
25	24	adantl 262	. . . . . . . . . . . . . . . . . 18 |- (((y e. RR /\ x e. RR) /\ z = -oo) -> (z < y <-> -oo < y))
26	23, 25	mpbird 156	. . . . . . . . . . . . . . . . 17 |- (((y e. RR /\ x e. RR) /\ z = -oo) -> z < y)
27	26	olcd 652	. . . . . . . . . . . . . . . 16 |- (((y e. RR /\ x e. RR) /\ z = -oo) -> (x < z \/ z < y))
28	27	a1d 22	. . . . . . . . . . . . . . 15 |- (((y e. RR /\ x e. RR) /\ z = -oo) -> (x < y -> (x < z \/ z < y)))
29	14, 21, 28	3jaodan 1200	. . . . . . . . . . . . . 14 |- (((y e. RR /\ x e. RR) /\ (z e. RR \/ z = +oo \/ z = -oo)) -> (x < y -> (x < z \/ z < y)))
30	9, 29	sylan2b 271	. . . . . . . . . . . . 13 |- (((y e. RR /\ x e. RR) /\ z e. RR*) -> (x < y -> (x < z \/ z < y)))
31	30	anasss 379	. . . . . . . . . . . 12 |- ((y e. RR /\ (x e. RR /\ z e. RR*)) -> (x < y -> (x < z \/ z < y)))
32	31	ancoms 255	. . . . . . . . . . 11 |- (((x e. RR /\ z e. RR*) /\ y e. RR) -> (x < y -> (x < z \/ z < y)))
33		ltpnf 8432	. . . . . . . . . . . . . . . . . . 19 |- (z e. RR -> z < +oo)
34	33	adantl 262	. . . . . . . . . . . . . . . . . 18 |- (((y = +oo /\ x e. RR) /\ z e. RR) -> z < +oo)
35		breq2 3759	. . . . . . . . . . . . . . . . . . 19 |- (y = +oo -> (z < y <-> z < +oo))
36	35	ad2antrr 457	. . . . . . . . . . . . . . . . . 18 |- (((y = +oo /\ x e. RR) /\ z e. RR) -> (z < y <-> z < +oo))
37	34, 36	mpbird 156	. . . . . . . . . . . . . . . . 17 |- (((y = +oo /\ x e. RR) /\ z e. RR) -> z < y)
38	37	olcd 652	. . . . . . . . . . . . . . . 16 |- (((y = +oo /\ x e. RR) /\ z e. RR) -> (x < z \/ z < y))
39	38	a1d 22	. . . . . . . . . . . . . . 15 |- (((y = +oo /\ x e. RR) /\ z e. RR) -> (x < y -> (x < z \/ z < y)))
40	15	ad2antlr 458	. . . . . . . . . . . . . . . . . 18 |- (((y = +oo /\ x e. RR) /\ z = +oo) -> x < +oo)
41	17	adantl 262	. . . . . . . . . . . . . . . . . 18 |- (((y = +oo /\ x e. RR) /\ z = +oo) -> (x < z <-> x < +oo))
42	40, 41	mpbird 156	. . . . . . . . . . . . . . . . 17 |- (((y = +oo /\ x e. RR) /\ z = +oo) -> x < z)
43	42	orcd 651	. . . . . . . . . . . . . . . 16 |- (((y = +oo /\ x e. RR) /\ z = +oo) -> (x < z \/ z < y))
44	43	a1d 22	. . . . . . . . . . . . . . 15 |- (((y = +oo /\ x e. RR) /\ z = +oo) -> (x < y -> (x < z \/ z < y)))
45		mnfltpnf 8436	. . . . . . . . . . . . . . . . . . 19 |- -oo < +oo
46		breq12 3760	. . . . . . . . . . . . . . . . . . . 20 |- ((z = -oo /\ y = +oo) -> (z < y <-> -oo < +oo))
47	46	ancoms 255	. . . . . . . . . . . . . . . . . . 19 |- ((y = +oo /\ z = -oo) -> (z < y <-> -oo < +oo))
48	45, 47	mpbiri 157	. . . . . . . . . . . . . . . . . 18 |- ((y = +oo /\ z = -oo) -> z < y)
49	48	adantlr 446	. . . . . . . . . . . . . . . . 17 |- (((y = +oo /\ x e. RR) /\ z = -oo) -> z < y)
50	49	olcd 652	. . . . . . . . . . . . . . . 16 |- (((y = +oo /\ x e. RR) /\ z = -oo) -> (x < z \/ z < y))
51	50	a1d 22	. . . . . . . . . . . . . . 15 |- (((y = +oo /\ x e. RR) /\ z = -oo) -> (x < y -> (x < z \/ z < y)))
52	39, 44, 51	3jaodan 1200	. . . . . . . . . . . . . 14 |- (((y = +oo /\ x e. RR) /\ (z e. RR \/ z = +oo \/ z = -oo)) -> (x < y -> (x < z \/ z < y)))
53	9, 52	sylan2b 271	. . . . . . . . . . . . 13 |- (((y = +oo /\ x e. RR) /\ z e. RR*) -> (x < y -> (x < z \/ z < y)))
54	53	anasss 379	. . . . . . . . . . . 12 |- ((y = +oo /\ (x e. RR /\ z e. RR*)) -> (x < y -> (x < z \/ z < y)))
55	54	ancoms 255	. . . . . . . . . . 11 |- (((x e. RR /\ z e. RR*) /\ y = +oo) -> (x < y -> (x < z \/ z < y)))
56		rexr 6828	. . . . . . . . . . . . . . 15 |- (x e. RR -> x e. RR*)
57		nltmnf 8439	. . . . . . . . . . . . . . 15 |- (x e. RR* -> -. x < -oo)
58	56, 57	syl 14	. . . . . . . . . . . . . 14 |- (x e. RR -> -. x < -oo)
59	58	ad2antrr 457	. . . . . . . . . . . . 13 |- (((x e. RR /\ z e. RR*) /\ y = -oo) -> -. x < -oo)
60		breq2 3759	. . . . . . . . . . . . . 14 |- (y = -oo -> (x < y <-> x < -oo))
61	60	adantl 262	. . . . . . . . . . . . 13 |- (((x e. RR /\ z e. RR*) /\ y = -oo) -> (x < y <-> x < -oo))
62	59, 61	mtbird 597	. . . . . . . . . . . 12 |- (((x e. RR /\ z e. RR*) /\ y = -oo) -> -. x < y)
63	62	pm2.21d 549	. . . . . . . . . . 11 |- (((x e. RR /\ z e. RR*) /\ y = -oo) -> (x < y -> (x < z \/ z < y)))
64	32, 55, 63	3jaodan 1200	. . . . . . . . . 10 |- (((x e. RR /\ z e. RR*) /\ (y e. RR \/ y = +oo \/ y = -oo)) -> (x < y -> (x < z \/ z < y)))
65	8, 64	sylan2b 271	. . . . . . . . 9 |- (((x e. RR /\ z e. RR*) /\ y e. RR*) -> (x < y -> (x < z \/ z < y)))
66	65	anasss 379	. . . . . . . 8 |- ((x e. RR /\ (z e. RR* /\ y e. RR*)) -> (x < y -> (x < z \/ z < y)))
67	66	ancoms 255	. . . . . . 7 |- (((z e. RR* /\ y e. RR*) /\ x e. RR) -> (x < y -> (x < z \/ z < y)))
68		pnfnlt 8438	. . . . . . . . . 10 |- (y e. RR* -> -. +oo < y)
69	68	ad2antlr 458	. . . . . . . . 9 |- (((z e. RR* /\ y e. RR*) /\ x = +oo) -> -. +oo < y)
70		breq1 3758	. . . . . . . . . 10 |- (x = +oo -> (x < y <-> +oo < y))
71	70	adantl 262	. . . . . . . . 9 |- (((z e. RR* /\ y e. RR*) /\ x = +oo) -> (x < y <-> +oo < y))
72	69, 71	mtbird 597	. . . . . . . 8 |- (((z e. RR* /\ y e. RR*) /\ x = +oo) -> -. x < y)
73	72	pm2.21d 549	. . . . . . 7 |- (((z e. RR* /\ y e. RR*) /\ x = +oo) -> (x < y -> (x < z \/ z < y)))
74		df-3or 885	. . . . . . . . . . 11 |- ((z e. RR \/ z = +oo \/ z = -oo) <-> ((z e. RR \/ z = +oo) \/ z = -oo))
75	9, 74	bitri 173	. . . . . . . . . 10 |- (z e. RR* <-> ((z e. RR \/ z = +oo) \/ z = -oo))
76		mnfltxr 8437	. . . . . . . . . . . . . . 15 |- ((z e. RR \/ z = +oo) -> -oo < z)
77	76	adantl 262	. . . . . . . . . . . . . 14 |- ((x = -oo /\ (z e. RR \/ z = +oo)) -> -oo < z)
78		breq1 3758	. . . . . . . . . . . . . . 15 |- (x = -oo -> (x < z <-> -oo < z))
79	78	adantr 261	. . . . . . . . . . . . . 14 |- ((x = -oo /\ (z e. RR \/ z = +oo)) -> (x < z <-> -oo < z))
80	77, 79	mpbird 156	. . . . . . . . . . . . 13 |- ((x = -oo /\ (z e. RR \/ z = +oo)) -> x < z)
81	80	orcd 651	. . . . . . . . . . . 12 |- ((x = -oo /\ (z e. RR \/ z = +oo)) -> (x < z \/ z < y))
82	81	a1d 22	. . . . . . . . . . 11 |- ((x = -oo /\ (z e. RR \/ z = +oo)) -> (x < y -> (x < z \/ z < y)))
83		eqtr3 2056	. . . . . . . . . . . . 13 |- ((x = -oo /\ z = -oo) -> x = z)
84	83	breq1d 3765	. . . . . . . . . . . 12 |- ((x = -oo /\ z = -oo) -> (x < y <-> z < y))
85		olc 631	. . . . . . . . . . . 12 |- (z < y -> (x < z \/ z < y))
86	84, 85	syl6bi 152	. . . . . . . . . . 11 |- ((x = -oo /\ z = -oo) -> (x < y -> (x < z \/ z < y)))
87	82, 86	jaodan 709	. . . . . . . . . 10 |- ((x = -oo /\ ((z e. RR \/ z = +oo) \/ z = -oo)) -> (x < y -> (x < z \/ z < y)))
88	75, 87	sylan2b 271	. . . . . . . . 9 |- ((x = -oo /\ z e. RR*) -> (x < y -> (x < z \/ z < y)))
89	88	ancoms 255	. . . . . . . 8 |- ((z e. RR* /\ x = -oo) -> (x < y -> (x < z \/ z < y)))
90	89	adantlr 446	. . . . . . 7 |- (((z e. RR* /\ y e. RR*) /\ x = -oo) -> (x < y -> (x < z \/ z < y)))
91	67, 73, 90	3jaodan 1200	. . . . . 6 |- (((z e. RR* /\ y e. RR*) /\ (x e. RR \/ x = +oo \/ x = -oo)) -> (x < y -> (x < z \/ z < y)))
92	91	3impa 1098	. . . . 5 |- ((z e. RR* /\ y e. RR* /\ (x e. RR \/ x = +oo \/ x = -oo)) -> (x < y -> (x < z \/ z < y)))
93	7, 92	syl3an3b 1172	. . . 4 |- ((z e. RR* /\ y e. RR* /\ x e. RR*) -> (x < y -> (x < z \/ z < y)))
94	93	3com13 1108	. . 3 |- ((x e. RR* /\ y e. RR* /\ z e. RR*) -> (x < y -> (x < z \/ z < y)))
95	94	rgen3 2400	. 2 |- A.x e. RR* A.y e. RR* A.z e. RR* (x < y -> (x < z \/ z < y))
96		df-iso 4025	. 2 |- ( < Or RR* <-> ( < Po RR* /\ A.x e. RR* A.y e. RR* A.z e. RR* (x < y -> (x < z \/ z < y))))
97	6, 95, 96	mpbir2an 848	1 |- < Or RR*

Syntax hints:  -. wn 3   -> wi 4   /\ wa 97   <-> wb 98   \/ wo 628   \/ w3o 883   /\ w3a 884   = wceq 1242   T. wtru 1243   e. wcel 1390  A.wral 2300   class class class wbr 3755   Po wpo 4022   Or wor 4023   RRcr 6670   +oocpnf 6814   -oocmnf 6815   RR*cxr 6816   < clt 6817

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-in1 544  ax-in2 545  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-bnd 1396  ax-4 1397  ax-13 1401  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  ax-un 4136  ax-setind 4220  ax-cnex 6734  ax-resscn 6735  ax-pre-ltirr 6755  ax-pre-ltwlin 6756  ax-pre-lttrn 6757

This theorem depends on definitions:  df-bi 110  df-3or 885  df-3an 886  df-tru 1245  df-fal 1248  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-ne 2203  df-nel 2204  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-po 4024  df-iso 4025  df-xp 4294  df-pnf 6819  df-mnf 6820  df-xr 6821  df-ltxr 6822

This theorem is referenced by:  xrlelttr  8452  xrltletr  8453  xrletr  8454