xrltso - Intuitionistic Logic Explorer

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

Theorem xrltso 9917

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 9900	. . . . 5
2	1	adantl 277	. . . 4 $/\$
3		xrlttr 9916	. . . . 5 $/\$ $/\$ $/\$
4	3	adantl 277	. . . 4 $/\$ $/\$ $/\$ $/\$
5	2, 4	ispod 4350	. . 3
6	5	mptru 1381	. 2
7		elxr 9897	. . . . 5 $\/$ $\/$
8		elxr 9897	. . . . . . . . . 10 $\/$ $\/$
9		elxr 9897	. . . . . . . . . . . . . 14 $\/$ $\/$
10		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$
11		simpll 527	. . . . . . . . . . . . . . . 16 $/\$ $/\$
12		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$
13		axltwlin 8139	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
14	10, 11, 12, 13	syl3anc 1249	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
15		ltpnf 9901	. . . . . . . . . . . . . . . . . . 19
16	15	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17		breq2 4047	. . . . . . . . . . . . . . . . . . 19
18	17	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	16, 18	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	orcd 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
21	20	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
22		mnflt 9904	. . . . . . . . . . . . . . . . . . 19
23	22	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
24		breq1 4046	. . . . . . . . . . . . . . . . . . 19
25	24	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
26	23, 25	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
27	26	olcd 735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
28	27	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
29	14, 21, 28	3jaodan 1318	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
30	9, 29	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
31	30	anasss 399	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
32	31	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
33		ltpnf 9901	. . . . . . . . . . . . . . . . . . 19
34	33	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
35		breq2 4047	. . . . . . . . . . . . . . . . . . 19
36	35	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
37	34, 36	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	37	olcd 735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
39	38	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
40	15	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
41	17	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
42	40, 41	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
43	42	orcd 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
44	43	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
45		mnfltpnf 9906	. . . . . . . . . . . . . . . . . . 19
46		breq12 4048	. . . . . . . . . . . . . . . . . . . 20 $/\$
47	46	ancoms 268	. . . . . . . . . . . . . . . . . . 19 $/\$
48	45, 47	mpbiri 168	. . . . . . . . . . . . . . . . . 18 $/\$
49	48	adantlr 477	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50	49	olcd 735	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
51	50	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
52	39, 44, 51	3jaodan 1318	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
53	9, 52	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
54	53	anasss 399	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
55	54	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
56		rexr 8117	. . . . . . . . . . . . . . 15
57		nltmnf 9909	. . . . . . . . . . . . . . 15
58	56, 57	syl 14	. . . . . . . . . . . . . 14
59	58	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$
60		breq2 4047	. . . . . . . . . . . . . 14
61	60	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$
62	59, 61	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$
63	62	pm2.21d 620	. . . . . . . . . . 11 $/\$ $/\$ $\/$
64	32, 55, 63	3jaodan 1318	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$ $\/$
65	8, 64	sylan2b 287	. . . . . . . . 9 $/\$ $/\$ $\/$
66	65	anasss 399	. . . . . . . 8 $/\$ $/\$ $\/$
67	66	ancoms 268	. . . . . . 7 $/\$ $/\$ $\/$
68		pnfnlt 9908	. . . . . . . . . 10
69	68	ad2antlr 489	. . . . . . . . 9 $/\$ $/\$
70		breq1 4046	. . . . . . . . . 10
71	70	adantl 277	. . . . . . . . 9 $/\$ $/\$
72	69, 71	mtbird 674	. . . . . . . 8 $/\$ $/\$
73	72	pm2.21d 620	. . . . . . 7 $/\$ $/\$ $\/$
74		df-3or 981	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
75	9, 74	bitri 184	. . . . . . . . . 10 $\/$ $\/$
76		mnfltxr 9907	. . . . . . . . . . . . . . 15 $\/$
77	76	adantl 277	. . . . . . . . . . . . . 14 $/\$ $\/$
78		breq1 4046	. . . . . . . . . . . . . . 15
79	78	adantr 276	. . . . . . . . . . . . . 14 $/\$ $\/$
80	77, 79	mpbird 167	. . . . . . . . . . . . 13 $/\$ $\/$
81	80	orcd 734	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
82	81	a1d 22	. . . . . . . . . . 11 $/\$ $\/$ $\/$
83		eqtr3 2224	. . . . . . . . . . . . 13 $/\$
84	83	breq1d 4053	. . . . . . . . . . . 12 $/\$
85		olc 712	. . . . . . . . . . . 12 $\/$
86	84, 85	biimtrdi 163	. . . . . . . . . . 11 $/\$ $\/$
87	82, 86	jaodan 798	. . . . . . . . . 10 $/\$ $\/$ $\/$ $\/$
88	75, 87	sylan2b 287	. . . . . . . . 9 $/\$ $\/$
89	88	ancoms 268	. . . . . . . 8 $/\$ $\/$
90	89	adantlr 477	. . . . . . 7 $/\$ $/\$ $\/$
91	67, 73, 90	3jaodan 1318	. . . . . 6 $/\$ $/\$ $\/$ $\/$ $\/$
92	91	3impa 1196	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$
93	7, 92	syl3an3b 1287	. . . 4 $/\$ $/\$ $\/$
94	93	3com13 1210	. . 3 $/\$ $/\$ $\/$
95	94	rgen3 2592	. 2 $\/$
96		df-iso 4343	. 2 $/\$ $\/$
97	6, 95, 96	mpbir2an 944	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 $\/$ w3o 979 $/\$ w3a 980

wceq 1372

wtru 1373

wcel 2175

wral 2483 class class class wbr 4043

wpo 4340

wor 4341

cr 7923

cpnf 8103

cmnf 8104

cxr 8105

clt 8106

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 615 ax-in2 616 ax-io 710 ax-5 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-13 2177 ax-14 2178 ax-ext 2186 ax-sep 4161 ax-pow 4217 ax-pr 4252 ax-un 4479 ax-setind 4584 ax-cnex 8015 ax-resscn 8016 ax-pre-ltirr 8036 ax-pre-ltwlin 8037 ax-pre-lttrn 8038

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1375 df-fal 1378 df-nf 1483 df-sb 1785 df-eu 2056 df-mo 2057 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-ne 2376 df-nel 2471 df-ral 2488 df-rex 2489 df-rab 2492 df-v 2773 df-dif 3167 df-un 3169 df-in 3171 df-ss 3178 df-pw 3617 df-sn 3638 df-pr 3639 df-op 3641 df-uni 3850 df-br 4044 df-opab 4105 df-po 4342 df-iso 4343 df-xp 4680 df-pnf 8108 df-mnf 8109 df-xr 8110 df-ltxr 8111

This theorem is referenced by: xrlelttr 9927 xrltletr 9928 xrletr 9929 xrmaxiflemlub 11530

W3C validator