axsltsolem1 - Mathbox for Scott Fenton

Mathbox for Scott Fenton

< Previous Next >
Related theorems
Unicode version

Theorem axsltsolem1 14006

Description: Lemma for axsltso 14007. The sign expansion relationship totally orders the surreal signs.

**Assertion**
Ref	Expression
axsltsolem1

**Proof of Theorem axsltsolem1**
Step	Hyp	Ref	Expression
1		1n0 5187	. . . . . . . 8
2		df-ne 2019	. . . . . . . 8
3	1, 2	mpbi 206	. . . . . . 7
4		eqtr2 1905	. . . . . . 7 $/\$
5	3, 4	mto 121	. . . . . 6 $/\$
6		1on 5182	. . . . . . . . 9
7		0elon 3716	. . . . . . . . 9
8		suc11 3773	. . . . . . . . . 10 $/\$
9		df-2o 5178	. . . . . . . . . . 11
10		df-1o 5177	. . . . . . . . . . 11
11	9, 10	eqeq12i 1897	. . . . . . . . . 10
12	8, 11	syl5bb 591	. . . . . . . . 9 $/\$
13	6, 7, 12	mp2an 761	. . . . . . . 8
14	1, 13	nemtbir 2099	. . . . . . 7
15		eqtr2 1905	. . . . . . . 8 $/\$
16	15	ancoms 484	. . . . . . 7 $/\$
17	14, 16	mto 121	. . . . . 6 $/\$
18		nsuceq0 3749	. . . . . . . 8
19	9	eqeq1i 1891	. . . . . . . 8
20	18, 19	nemtbir 2099	. . . . . . 7
21		eqtr2 1905	. . . . . . . 8 $/\$
22	21	ancoms 484	. . . . . . 7 $/\$
23	20, 22	mto 121	. . . . . 6 $/\$
24	5, 17, 23	3pm3.2ni 13809	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
25		visset 2295	. . . . . 6
26		0ex 3446	. . . . . 6
27		2on 5183	. . . . . . 7
28	27	elisseti 2301	. . . . . 6
29	25, 25, 26, 28, 28	brtp 13830	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
30	24, 29	mtbir 209	. . . 4
31	30	a1i 8	. . 3
32		eqtr2 1905	. . . . . . . . . . . 12 $/\$
33	3, 32	mto 121	. . . . . . . . . . 11 $/\$
34	33	pm2.21i 93	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
35	34	ad2ant2rl 447	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
36	35	expcom 403	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
37	34	ad2ant2rl 447	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
38	37	expcom 403	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
39		3mix2 1046	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
40	39	ad2ant2rl 447	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
41	40	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
42	36, 38, 41	3jaod 1161	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
43		eqtr2 1905	. . . . . . . . . . . 12 $/\$
44	14, 43	mto 121	. . . . . . . . . . 11 $/\$
45	44	pm2.21i 93	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
46	45	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
47	46	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
48	45	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
49	48	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
50		eqtr2 1905	. . . . . . . . . . . 12 $/\$
51	20, 50	mto 121	. . . . . . . . . . 11 $/\$
52	51	pm2.21i 93	. . . . . . . . . 10 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
53	52	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
54	53	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
55	47, 49, 54	3jaod 1161	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
56	45	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
57	56	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
58	45	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
59	58	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
60	52	ad2ant2lr 446	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
61	60	ex 402	. . . . . . . 8 $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
62	57, 59, 61	3jaod 1161	. . . . . . 7 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
63	42, 55, 62	3jaoi 1160	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
64	63	imp 377	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
65		visset 2295	. . . . . . 7
66	25, 65, 26, 28, 28	brtp 13830	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$
67		visset 2295	. . . . . . 7
68	65, 67, 26, 28, 28	brtp 13830	. . . . . 6 $/\$ $\/$ $/\$ $\/$ $/\$
69	66, 68	anbi12i 540	. . . . 5 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
70	25, 67, 26, 28, 28	brtp 13830	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
71	64, 69, 70	3imtr4i 236	. . . 4 $/\$
72	71	a1i 8	. . 3 $/\$ $/\$ $/\$
73		eqtr3 1907	. . . . . . . . 9 $/\$
74	73	3mix2d 13813	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
75	74	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
76		3mix2 1046	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
77	76	3mix1d 13812	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
78	77	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
79		3mix1 1045	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
80	79	3mix1d 13812	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
81	80	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
82	75, 78, 81	3jaod 1161	. . . . . 6 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
83		3mix2 1046	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
84	83	3mix3d 13814	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
85	84	expcom 403	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
86		eqtr3 1907	. . . . . . . . 9 $/\$
87	86	3mix2d 13813	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
88	87	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
89		3mix3 1047	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
90	89	3mix3d 13814	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
91	90	expcom 403	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
92	85, 88, 91	3jaod 1161	. . . . . 6 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
93		3mix1 1045	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
94	93	3mix3d 13814	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
95	94	expcom 403	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
96		3mix3 1047	. . . . . . . . 9 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
97	96	3mix1d 13812	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
98	97	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
99		eqtr3 1907	. . . . . . . . 9 $/\$
100	99	3mix2d 13813	. . . . . . . 8 $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
101	100	ex 402	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
102	95, 98, 101	3jaod 1161	. . . . . 6 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
103	82, 92, 102	3jaoi 1160	. . . . 5 $\/$ $\/$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
104	103	imp 377	. . . 4 $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
105	25	eltp 3074	. . . . 5 $\/$ $\/$
106	65	eltp 3074	. . . . 5 $\/$ $\/$
107	105, 106	anbi12i 540	. . . 4 $/\$ $\/$ $\/$ $/\$ $\/$ $\/$
108		biid 187	. . . . 5
109	65, 25, 26, 28, 28	brtp 13830	. . . . 5 $/\$ $\/$ $/\$ $\/$ $/\$
110	66, 108, 109	3orbi123i 1057	. . . 4 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
111	104, 107, 110	3imtr4i 236	. . 3 $/\$ $\/$ $\/$
112	31, 72, 111	itlso 3619	. 2
113		df-tp 3052	. . 3
114		soeq2 3609	. . 3
115	113, 114	ax-mp 7	. 2
116	112, 115	mpbi 206	1

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $/\$ wa 240 $\/$ w3o 857 $/\$ w3a 858

wceq 1298

wcel 1300

wne 2017

cun 2591

c0 2875

csn 3044

cpr 3045

cop 3046

ctp 3051 class class class wbr 3338

wor 3590

con0 3657

csuc 3659

c1o 5172

c2o 5173

This theorem is referenced by: axsltso 14007

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-pss 2607 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-tp 3052 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-tr 3412 df-eprel 3583 df-po 3591 df-so 3604 df-fr 3625 df-we 3644 df-ord 3660 df-on 3661 df-suc 3663 df-1o 5177 df-2o 5178