xrltso - Intuitionistic Logic Explorer

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

Theorem xrltso 9862

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 9845	. . . . 5
2	1	adantl 277	. . . 4 $/\$
3		xrlttr 9861	. . . . 5 $/\$ $/\$ $/\$
4	3	adantl 277	. . . 4 $/\$ $/\$ $/\$ $/\$
5	2, 4	ispod 4335	. . 3
6	5	mptru 1373	. 2
7		elxr 9842	. . . . 5 $\/$ $\/$
8		elxr 9842	. . . . . . . . . 10 $\/$ $\/$
9		elxr 9842	. . . . . . . . . . . . . 14 $\/$ $\/$
10		simplr 528	. . . . . . . . . . . . . . . 16 $/\$ $/\$
11		simpll 527	. . . . . . . . . . . . . . . 16 $/\$ $/\$
12		simpr 110	. . . . . . . . . . . . . . . 16 $/\$ $/\$
13		axltwlin 8087	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
14	10, 11, 12, 13	syl3anc 1249	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
15		ltpnf 9846	. . . . . . . . . . . . . . . . . . 19
16	15	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17		breq2 4033	. . . . . . . . . . . . . . . . . . 19
18	17	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	16, 18	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	orcd 734	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
21	20	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
22		mnflt 9849	. . . . . . . . . . . . . . . . . . 19
23	22	ad2antrr 488	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
24		breq1 4032	. . . . . . . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
30	9, 29	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
31	30	anasss 399	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
32	31	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
33		ltpnf 9846	. . . . . . . . . . . . . . . . . . 19
34	33	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
35		breq2 4033	. . . . . . . . . . . . . . . . . . 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 9851	. . . . . . . . . . . . . . . . . . 19
46		breq12 4034	. . . . . . . . . . . . . . . . . . . 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 1317	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
53	9, 52	sylan2b 287	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
54	53	anasss 399	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
55	54	ancoms 268	. . . . . . . . . . 11 $/\$ $/\$ $\/$
56		rexr 8065	. . . . . . . . . . . . . . 15
57		nltmnf 9854	. . . . . . . . . . . . . . 15
58	56, 57	syl 14	. . . . . . . . . . . . . 14
59	58	ad2antrr 488	. . . . . . . . . . . . 13 $/\$ $/\$
60		breq2 4033	. . . . . . . . . . . . . 14
61	60	adantl 277	. . . . . . . . . . . . 13 $/\$ $/\$
62	59, 61	mtbird 674	. . . . . . . . . . . 12 $/\$ $/\$
63	62	pm2.21d 620	. . . . . . . . . . 11 $/\$ $/\$ $\/$
64	32, 55, 63	3jaodan 1317	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$ $\/$
65	8, 64	sylan2b 287	. . . . . . . . 9 $/\$ $/\$ $\/$
66	65	anasss 399	. . . . . . . 8 $/\$ $/\$ $\/$
67	66	ancoms 268	. . . . . . 7 $/\$ $/\$ $\/$
68		pnfnlt 9853	. . . . . . . . . 10
69	68	ad2antlr 489	. . . . . . . . 9 $/\$ $/\$
70		breq1 4032	. . . . . . . . . 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 9852	. . . . . . . . . . . . . . 15 $\/$
77	76	adantl 277	. . . . . . . . . . . . . 14 $/\$ $\/$
78		breq1 4032	. . . . . . . . . . . . . . 15
79	78	adantr 276	. . . . . . . . . . . . . 14 $/\$ $\/$
80	77, 79	mpbird 167	. . . . . . . . . . . . 13 $/\$ $\/$
81	80	orcd 734	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
82	81	a1d 22	. . . . . . . . . . 11 $/\$ $\/$ $\/$
83		eqtr3 2213	. . . . . . . . . . . . 13 $/\$
84	83	breq1d 4039	. . . . . . . . . . . 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 1317	. . . . . 6 $/\$ $/\$ $\/$ $\/$ $\/$
92	91	3impa 1196	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$
93	7, 92	syl3an3b 1287	. . . 4 $/\$ $/\$ $\/$
94	93	3com13 1210	. . 3 $/\$ $/\$ $\/$
95	94	rgen3 2581	. 2 $\/$
96		df-iso 4328	. 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 1364

wtru 1365

wcel 2164

wral 2472 class class class wbr 4029

wpo 4325

wor 4326

cr 7871

cpnf 8051

cmnf 8052

cxr 8053

clt 8054

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 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2166 ax-14 2167 ax-ext 2175 ax-sep 4147 ax-pow 4203 ax-pr 4238 ax-un 4464 ax-setind 4569 ax-cnex 7963 ax-resscn 7964 ax-pre-ltirr 7984 ax-pre-ltwlin 7985 ax-pre-lttrn 7986

This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2045 df-mo 2046 df-clab 2180 df-cleq 2186 df-clel 2189 df-nfc 2325 df-ne 2365 df-nel 2460 df-ral 2477 df-rex 2478 df-rab 2481 df-v 2762 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-pw 3603 df-sn 3624 df-pr 3625 df-op 3627 df-uni 3836 df-br 4030 df-opab 4091 df-po 4327 df-iso 4328 df-xp 4665 df-pnf 8056 df-mnf 8057 df-xr 8058 df-ltxr 8059

This theorem is referenced by: xrlelttr 9872 xrltletr 9873 xrletr 9874 xrmaxiflemlub 11391

W3C validator