cdleme20l2 - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdleme20l2		Structured version Unicode version

Theorem cdleme20l2 31055

Description: Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line.

represent s₂, f(s), t₂, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

**Hypotheses**
Ref	Expression
cdleme19.l
cdleme19.j	$.\/$
cdleme19.m	$./\$
cdleme19.a
cdleme19.h
cdleme19.u	$.\/$ $./\$
cdleme19.f	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme19.g	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdleme19.d	$.\/$ $./\$
cdleme19.y	$.\/$ $./\$
cdleme20.v	$.\/$ $./\$

**Assertion**
Ref	Expression
cdleme20l2	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

**Proof of Theorem cdleme20l2**
Step	Hyp	Ref	Expression
1		simp11l 1068	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		hllat 30098	. . . . 5
3	1, 2	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp11r 1069	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		simp12l 1070	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		simp13l 1072	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
7		simp22l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
8		cdleme19.l	. . . . . 6
9		cdleme19.j	. . . . . 6 $.\/$
10		cdleme19.m	. . . . . 6 $./\$
11		cdleme19.a	. . . . . 6
12		cdleme19.h	. . . . . 6
13		cdleme19.u	. . . . . 6 $.\/$ $./\$
14		cdleme19.f	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
15		eqid 2435	. . . . . 6
16	8, 9, 10, 11, 12, 13, 14, 15	cdleme1b 30960	. . . . 5 $/\$ $/\$ $/\$ $/\$
17	1, 4, 5, 6, 7, 16	syl23anc 1191	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
18		simp21l 1074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
19		cdleme19.d	. . . . . 6 $.\/$ $./\$
20	8, 9, 10, 11, 12, 19, 15	cdlemedb 31031	. . . . 5 $/\$ $/\$ $/\$
21	1, 4, 18, 7, 20	syl22anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
22		simp23l 1078	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
23		cdleme19.g	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
24	8, 9, 10, 11, 12, 13, 23, 15	cdleme1b 30960	. . . . 5 $/\$ $/\$ $/\$ $/\$
25	1, 4, 5, 6, 22, 24	syl23anc 1191	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
26		cdleme19.y	. . . . . 6 $.\/$ $./\$
27	8, 9, 10, 11, 12, 26, 15	cdlemedb 31031	. . . . 5 $/\$ $/\$ $/\$
28	1, 4, 18, 22, 27	syl22anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
29	15, 9	latj4 14522	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
30	3, 17, 21, 25, 28, 29	syl122anc 1193	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31		simp1 957	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp22 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
33		simp23 992	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
34		simp21 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
35		simp31 993	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
36		simp321 1107	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simp322 1108	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
38	36, 37	jca 519	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
39		simp323 1109	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40		cdleme20.v	. . . . . . 7 $.\/$ $./\$
41	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20d 31046	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42	31, 32, 33, 34, 35, 38, 39, 41	syl133anc 1207	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
43		simp22r 1077	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44		simp31r 1081	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	8, 9, 10, 11, 12, 40	lhpat2 30779	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 4, 7, 43, 22, 44, 45	syl222anc 1200	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
47	42, 46	eqeltrd 2509	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
48		simp11 987	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
49		simp12 988	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
50		simp13 989	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
51		simp31l 1080	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
52	8, 9, 10, 11, 12, 13, 14	cdleme3fa 30970	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53	48, 49, 50, 32, 51, 36, 52	syl132anc 1202	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
54	8, 9, 10, 11, 12, 13, 23	cdleme3fa 30970	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	48, 49, 50, 33, 51, 37, 54	syl132anc 1202	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
56		simp33r 1085	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
57	8, 9, 10, 11, 12, 13, 14, 23	cdleme16b 31013	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
58	31, 32, 33, 35, 36, 37, 56, 57	syl133anc 1207	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
59		eqid 2435	. . . . . . 7
60	9, 11, 59	llni2 30246	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
61	1, 53, 55, 58, 60	syl31anc 1187	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
62	8, 9, 10, 11, 12, 19	cdlemeda 31032	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
63	1, 4, 7, 43, 18, 39, 36, 62	syl223anc 1210	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
64		simp23r 1079	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
65	8, 9, 10, 11, 12, 26	cdlemeda 31032	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
66	1, 4, 22, 64, 18, 39, 37, 65	syl223anc 1210	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
67		simp32 994	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
68		simp33l 1084	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
69	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20j 31052	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
70	48, 49, 50, 34, 32, 33, 35, 67, 68, 69	syl333anc 1216	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
71	9, 11, 59	llni2 30246	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
72	1, 63, 66, 70, 71	syl31anc 1187	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
73		eqid 2435	. . . . . 6
74	9, 10, 11, 59, 73	2llnmj 30294	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
75	1, 61, 72, 74	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
76	47, 75	mpbid 202	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
77	30, 76	eqeltrd 2509	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
78	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20l1 31054	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	48, 49, 50, 18, 7, 43, 51, 36, 39, 78	syl333anc 1216	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80		eqid 2435	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
81	8, 9, 10, 11, 12, 13, 23, 14, 26, 19, 80	cdleme20l1 31054	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
82	48, 49, 50, 18, 22, 64, 51, 37, 39, 81	syl333anc 1216	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
83	9, 10, 11, 59, 73	2llnmj 30294	. . 3 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
84	1, 79, 82, 83	syl3anc 1184	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
85	77, 84	mpbird 224	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1652

wcel 1725

wne 2598 class class class wbr 4204

cfv 5446 (class class class)co 6073

cbs 13461

cple 13528

cjn 14393

cmee 14394

clat 14466

catm 29998

chlt 30085

clln 30225

clpl 30226

clh 30718

This theorem is referenced by: cdleme20l 31056

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1555 ax-5 1566 ax-17 1626 ax-9 1666 ax-8 1687 ax-13 1727 ax-14 1729 ax-6 1744 ax-7 1749 ax-11 1761 ax-12 1950 ax-ext 2416 ax-rep 4312 ax-sep 4322 ax-nul 4330 ax-pow 4369 ax-pr 4395 ax-un 4693

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1328 df-ex 1551 df-nf 1554 df-sb 1659 df-eu 2284 df-mo 2285 df-clab 2422 df-cleq 2428 df-clel 2431 df-nfc 2560 df-ne 2600 df-nel 2601 df-ral 2702 df-rex 2703 df-reu 2704 df-rab 2706 df-v 2950 df-sbc 3154 df-csb 3244 df-dif 3315 df-un 3317 df-in 3319 df-ss 3326 df-nul 3621 df-if 3732 df-pw 3793 df-sn 3812 df-pr 3813 df-op 3815 df-uni 4008 df-iun 4087 df-iin 4088 df-br 4205 df-opab 4259 df-mpt 4260 df-id 4490 df-xp 4876 df-rel 4877 df-cnv 4878 df-co 4879 df-dm 4880 df-rn 4881 df-res 4882 df-ima 4883 df-iota 5410 df-fun 5448 df-fn 5449 df-f 5450 df-f1 5451 df-fo 5452 df-f1o 5453 df-fv 5454 df-ov 6076 df-oprab 6077 df-mpt2 6078 df-1st 6341 df-2nd 6342 df-undef 6535 df-riota 6541 df-poset 14395 df-plt 14407 df-lub 14423 df-glb 14424 df-join 14425 df-meet 14426 df-p0 14460 df-p1 14461 df-lat 14467 df-clat 14529 df-oposet 29911 df-ol 29913 df-oml 29914 df-covers 30001 df-ats 30002 df-atl 30033 df-cvlat 30057 df-hlat 30086 df-llines 30232 df-lplanes 30233 df-lvols 30234 df-lines 30235 df-psubsp 30237 df-pmap 30238 df-padd 30530 df-lhyp 30722

W3C validator