xrltso - Intuitionistic Logic Explorer

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

Theorem xrltso 8717

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 8701	. . . . 5
2	1	adantl 262	. . . 4 $/\$
3		xrlttr 8716	. . . . 5 $/\$ $/\$ $/\$
4	3	adantl 262	. . . 4 $/\$ $/\$ $/\$ $/\$
5	2, 4	ispod 4041	. . 3
6	5	trud 1252	. 2
7		elxr 8696	. . . . 5 $\/$ $\/$
8		elxr 8696	. . . . . . . . . 10 $\/$ $\/$
9		elxr 8696	. . . . . . . . . . . . . 14 $\/$ $\/$
10		simplr 482	. . . . . . . . . . . . . . . 16 $/\$ $/\$
11		simpll 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
12		simpr 103	. . . . . . . . . . . . . . . 16 $/\$ $/\$
13		axltwlin 7087	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
14	10, 11, 12, 13	syl3anc 1135	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
15		ltpnf 8702	. . . . . . . . . . . . . . . . . . 19
16	15	ad2antlr 458	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
17		breq2 3768	. . . . . . . . . . . . . . . . . . 19
18	17	adantl 262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
19	16, 18	mpbird 156	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
20	19	orcd 652	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
21	20	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
22		mnflt 8704	. . . . . . . . . . . . . . . . . . 19
23	22	ad2antrr 457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
24		breq1 3767	. . . . . . . . . . . . . . . . . . 19
25	24	adantl 262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
26	23, 25	mpbird 156	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
27	26	olcd 653	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
28	27	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
29	14, 21, 28	3jaodan 1201	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
30	9, 29	sylan2b 271	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
31	30	anasss 379	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
32	31	ancoms 255	. . . . . . . . . . 11 $/\$ $/\$ $\/$
33		ltpnf 8702	. . . . . . . . . . . . . . . . . . 19
34	33	adantl 262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
35		breq2 3768	. . . . . . . . . . . . . . . . . . 19
36	35	ad2antrr 457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
37	34, 36	mpbird 156	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
38	37	olcd 653	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
39	38	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
40	15	ad2antlr 458	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
41	17	adantl 262	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
42	40, 41	mpbird 156	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
43	42	orcd 652	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
44	43	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
45		mnfltpnf 8706	. . . . . . . . . . . . . . . . . . 19
46		breq12 3769	. . . . . . . . . . . . . . . . . . . 20 $/\$
47	46	ancoms 255	. . . . . . . . . . . . . . . . . . 19 $/\$
48	45, 47	mpbiri 157	. . . . . . . . . . . . . . . . . 18 $/\$
49	48	adantlr 446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
50	49	olcd 653	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\/$
51	50	a1d 22	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\/$
52	39, 44, 51	3jaodan 1201	. . . . . . . . . . . . . 14 $/\$ $/\$ $\/$ $\/$ $\/$
53	9, 52	sylan2b 271	. . . . . . . . . . . . 13 $/\$ $/\$ $\/$
54	53	anasss 379	. . . . . . . . . . . 12 $/\$ $/\$ $\/$
55	54	ancoms 255	. . . . . . . . . . 11 $/\$ $/\$ $\/$
56		rexr 7071	. . . . . . . . . . . . . . 15
57		nltmnf 8709	. . . . . . . . . . . . . . 15
58	56, 57	syl 14	. . . . . . . . . . . . . 14
59	58	ad2antrr 457	. . . . . . . . . . . . 13 $/\$ $/\$
60		breq2 3768	. . . . . . . . . . . . . 14
61	60	adantl 262	. . . . . . . . . . . . 13 $/\$ $/\$
62	59, 61	mtbird 598	. . . . . . . . . . . 12 $/\$ $/\$
63	62	pm2.21d 549	. . . . . . . . . . 11 $/\$ $/\$ $\/$
64	32, 55, 63	3jaodan 1201	. . . . . . . . . 10 $/\$ $/\$ $\/$ $\/$ $\/$
65	8, 64	sylan2b 271	. . . . . . . . 9 $/\$ $/\$ $\/$
66	65	anasss 379	. . . . . . . 8 $/\$ $/\$ $\/$
67	66	ancoms 255	. . . . . . 7 $/\$ $/\$ $\/$
68		pnfnlt 8708	. . . . . . . . . 10
69	68	ad2antlr 458	. . . . . . . . 9 $/\$ $/\$
70		breq1 3767	. . . . . . . . . 10
71	70	adantl 262	. . . . . . . . 9 $/\$ $/\$
72	69, 71	mtbird 598	. . . . . . . 8 $/\$ $/\$
73	72	pm2.21d 549	. . . . . . 7 $/\$ $/\$ $\/$
74		df-3or 886	. . . . . . . . . . 11 $\/$ $\/$ $\/$ $\/$
75	9, 74	bitri 173	. . . . . . . . . 10 $\/$ $\/$
76		mnfltxr 8707	. . . . . . . . . . . . . . 15 $\/$
77	76	adantl 262	. . . . . . . . . . . . . 14 $/\$ $\/$
78		breq1 3767	. . . . . . . . . . . . . . 15
79	78	adantr 261	. . . . . . . . . . . . . 14 $/\$ $\/$
80	77, 79	mpbird 156	. . . . . . . . . . . . 13 $/\$ $\/$
81	80	orcd 652	. . . . . . . . . . . 12 $/\$ $\/$ $\/$
82	81	a1d 22	. . . . . . . . . . 11 $/\$ $\/$ $\/$
83		eqtr3 2059	. . . . . . . . . . . . 13 $/\$
84	83	breq1d 3774	. . . . . . . . . . . 12 $/\$
85		olc 632	. . . . . . . . . . . 12 $\/$
86	84, 85	syl6bi 152	. . . . . . . . . . 11 $/\$ $\/$
87	82, 86	jaodan 710	. . . . . . . . . 10 $/\$ $\/$ $\/$ $\/$
88	75, 87	sylan2b 271	. . . . . . . . 9 $/\$ $\/$
89	88	ancoms 255	. . . . . . . 8 $/\$ $\/$
90	89	adantlr 446	. . . . . . 7 $/\$ $/\$ $\/$
91	67, 73, 90	3jaodan 1201	. . . . . 6 $/\$ $/\$ $\/$ $\/$ $\/$
92	91	3impa 1099	. . . . 5 $/\$ $/\$ $\/$ $\/$ $\/$
93	7, 92	syl3an3b 1173	. . . 4 $/\$ $/\$ $\/$
94	93	3com13 1109	. . 3 $/\$ $/\$ $\/$
95	94	rgen3 2406	. 2 $\/$
96		df-iso 4034	. 2 $/\$ $\/$
97	6, 95, 96	mpbir2an 849	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 97

wb 98 $\/$ wo 629 $\/$ w3o 884 $/\$ w3a 885

wceq 1243

wtru 1244

wcel 1393

wral 2306 class class class wbr 3764

wpo 4031

wor 4032

cr 6888

cpnf 7057

cmnf 7058

cxr 7059

clt 7060

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 630 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-10 1396 ax-11 1397 ax-i12 1398 ax-bndl 1399 ax-4 1400 ax-13 1404 ax-14 1405 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-sep 3875 ax-pow 3927 ax-pr 3944 ax-un 4170 ax-setind 4262 ax-cnex 6975 ax-resscn 6976 ax-pre-ltirr 6996 ax-pre-ltwlin 6997 ax-pre-lttrn 6998

This theorem depends on definitions: df-bi 110 df-3or 886 df-3an 887 df-tru 1246 df-fal 1249 df-nf 1350 df-sb 1646 df-eu 1903 df-mo 1904 df-clab 2027 df-cleq 2033 df-clel 2036 df-nfc 2167 df-ne 2206 df-nel 2207 df-ral 2311 df-rex 2312 df-rab 2315 df-v 2559 df-dif 2920 df-un 2922 df-in 2924 df-ss 2931 df-pw 3361 df-sn 3381 df-pr 3382 df-op 3384 df-uni 3581 df-br 3765 df-opab 3819 df-po 4033 df-iso 4034 df-xp 4351 df-pnf 7062 df-mnf 7063 df-xr 7064 df-ltxr 7065

This theorem is referenced by: xrlelttr 8722 xrltletr 8723 xrletr 8724

W3C validator