xrltso - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > xrltso		Unicode version

Theorem xrltso 10177

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

**Assertion**
Ref	Expression
xrltso

Proof of Theorem xrltso Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xrltnr 10160	. . . . 5
2	1	adantl 277	. . . 4 $/\$
3		xrlttr 10176	. . . . 5 $/\$ $/\$ $/\$
4	3	adantl 277	. . . 4 $/\$ $/\$ $/\$ $/\$
5	2, 4	ispod 4444	. . 3
6	5	mptru 1411	. 2
7		elxr 10157	. . . . 5 $\/$ $\/$
8		elxr 10157	. . . . . . . . . 10 $\/$ $\/$
9		elxr 10157	. . . . . . . . . . . . . 14 $\/$ $\/$
10		simplr 533	. . . . . . . . . . . . . . . 16 $/\$ $/\$
11		simpll 531	. . . . . . . . . . . . . . . 16 $/\$ $/\$
12		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$
13		axltwlin 8383	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
14	10, 11, 12, 13	syl3anc 1278	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
15		ltpnf 10161	. . . . . . . . . . . . . . . . . . 19
16	15	ad2antlr 493	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17		breq2 4129	. . . . . . . . . . . . . . . . . . 19
18	17	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	16, 18	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	orcd 745	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
21	20	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
22		mnflt 10164	. . . . . . . . . . . . . . . . . . 19
23	22	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
24		breq1 4128	. . . . . . . . . . . . . . . . . . 19
25	24	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
26	23, 25	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
27	26	olcd 746	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
28	27	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
29	14, 21, 28	3jaodan 1347	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
30	9, 29	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
31	30	anasss 403	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
32	31	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
33		ltpnf 10161	. . . . . . . . . . . . . . . . . . 19
34	33	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
35		breq2 4129	. . . . . . . . . . . . . . . . . . 19
36	35	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
37	34, 36	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	37	olcd 746	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
39	38	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
40	15	ad2antlr 493	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
41	17	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
42	40, 41	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
43	42	orcd 745	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
44	43	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
45		mnfltpnf 10166	. . . . . . . . . . . . . . . . . . 19
46		breq12 4130	. . . . . . . . . . . . . . . . . . . 20 $/\$
47	46	ancoms 268	. . . . . . . . . . . . . . . . . . 19 $/\$
48	45, 47	mpbiri 168	. . . . . . . . . . . . . . . . . 18 $/\$
49	48	adantlr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50	49	olcd 746	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
51	50	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
52	39, 44, 51	3jaodan 1347	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
53	9, 52	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
54	53	anasss 403	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
55	54	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
56		rexr 8361	. . . . . . . . . . . . . . 15
57		nltmnf 10169	. . . . . . . . . . . . . . 15
58	56, 57	syl 14	. . . . . . . . . . . . . 14
59	58	ad2antrr 492	. . . . . . . . . . . . 13 $/\$ $/\$
60		breq2 4129	. . . . . . . . . . . . . 14
61	60	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$
62	59, 61	mtbird 684	. . . . . . . . . . . 12 $/\$ $/\$
63	62	pm2.21d 628	. . . . . . . . . . 11 $/\$ $/\$ $\/$
64	32, 55, 63	3jaodan 1347	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$ $\/$
65	8, 64	sylan2b 287	. . . . . . . . 9 $/\$ $/\$ $\/$
66	65	anasss 403	. . . . . . . 8 $/\$ $/\$ $\/$
67	66	ancoms 268	. . . . . . 7 $/\$ $/\$ $\/$
68		pnfnlt 10168	. . . . . . . . . 10
69	68	ad2antlr 493	. . . . . . . . 9 $/\$ $/\$
70		breq1 4128	. . . . . . . . . 10
71	70	adantl 277	. . . . . . . . 9 $/\$ $/\$
72	69, 71	mtbird 684	. . . . . . . 8 $/\$ $/\$
73	72	pm2.21d 628	. . . . . . 7 $/\$ $/\$ $\/$
74		df-3or 1010	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
75	9, 74	bitri 184	. . . . . . . . . 10 $\/$ $\/$
76		mnfltxr 10167	. . . . . . . . . . . . . . 15 $\/$
77	76	adantl 277	. . . . . . . . . . . . . 14 $/\$ $\/$
78		breq1 4128	. . . . . . . . . . . . . . 15
79	78	adantr 276	. . . . . . . . . . . . . 14 $/\$ $\/$
80	77, 79	mpbird 167	. . . . . . . . . . . . 13 $/\$ $\/$
81	80	orcd 745	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
82	81	a1d 22	. . . . . . . . . . 11 $/\$ $\/$ $\/$
83		eqtr3 2258	. . . . . . . . . . . . 13 $/\$
84	83	breq1d 4135	. . . . . . . . . . . 12 $/\$
85		olc 723	. . . . . . . . . . . 12 $\/$
86	84, 85	biimtrdi 163	. . . . . . . . . . 11 $/\$ $\/$
87	82, 86	jaodan 809	. . . . . . . . . 10 $/\$ $\/$ $\/$ $\/$
88	75, 87	sylan2b 287	. . . . . . . . 9 $/\$ $\/$
89	88	ancoms 268	. . . . . . . 8 $/\$ $\/$
90	89	adantlr 481	. . . . . . 7 $/\$ $/\$ $\/$
91	67, 73, 90	3jaodan 1347	. . . . . 6 $/\$ $/\$ $\/$ $\/$ $\/$
92	91	3impa 1225	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$
93	7, 92	syl3an3b 1316	. . . 4 $/\$ $/\$ $\/$
94	93	3com13 1239	. . 3 $/\$ $/\$ $\/$
95	94	rgen3 2637	. 2 $\/$
96		df-iso 4437	. 2 $/\$ $\/$
97	6, 95, 96	mpbir2an 955	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 $\/$ w3o 1008 $/\$ w3a 1009

wceq 1402

wtru 1403

wcel 2209

wral 2528 class class class wbr 4125

wpo 4434

wor 4435

cr 8168

cpnf 8347

cmnf 8348

cxr 8349

clt 8350

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4244 ax-pow 4306 ax-pr 4341 ax-un 4573 ax-setind 4679 ax-cnex 8260 ax-resscn 8261 ax-pre-ltirr 8281 ax-pre-ltwlin 8282 ax-pre-lttrn 8283

This theorem depends on definitions: df-bi 117 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-rab 2537 df-v 2823 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-pw 3687 df-sn 3711 df-pr 3712 df-op 3714 df-uni 3931 df-br 4126 df-opab 4188 df-po 4436 df-iso 4437 df-xp 4775 df-pnf 8352 df-mnf 8353 df-xr 8354 df-ltxr 8355

This theorem is referenced by: xrlelttr 10187 xrltletr 10188 xrletr 10189 xrmaxiflemlub 11992

W3C validator