cdleme20l2 - Mathbox for Norm Megill

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

Theorem cdleme20l2 29789

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 1066	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		hllat 28832	. . . . 5
3	1, 2	syl 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp11r 1067	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		simp12l 1068	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		simp13l 1070	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
7		simp22l 1074	. . . . 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 2284	. . . . . 6
16	8, 9, 10, 11, 12, 13, 14, 15	cdleme1b 29694	. . . . 5 $/\$ $/\$ $/\$ $/\$
17	1, 4, 5, 6, 7, 16	syl23anc 1189	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
18		simp21l 1072	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
19		cdleme19.d	. . . . . 6 $.\/$ $./\$
20	8, 9, 10, 11, 12, 19, 15	cdlemedb 29765	. . . . 5 $/\$ $/\$ $/\$
21	1, 4, 18, 7, 20	syl22anc 1183	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
22		simp23l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
23		cdleme19.g	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
24	8, 9, 10, 11, 12, 13, 23, 15	cdleme1b 29694	. . . . 5 $/\$ $/\$ $/\$ $/\$
25	1, 4, 5, 6, 22, 24	syl23anc 1189	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
26		cdleme19.y	. . . . . 6 $.\/$ $./\$
27	8, 9, 10, 11, 12, 26, 15	cdlemedb 29765	. . . . 5 $/\$ $/\$ $/\$
28	1, 4, 18, 22, 27	syl22anc 1183	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
29	15, 9	latj4 14203	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
30	3, 17, 21, 25, 28, 29	syl122anc 1191	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31		simp1 955	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp22 989	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
33		simp23 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
34		simp21 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
35		simp31 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
36		simp321 1105	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simp322 1106	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
38	36, 37	jca 518	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
39		simp323 1107	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40		cdleme20.v	. . . . . . 7 $.\/$ $./\$
41	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20d 29780	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42	31, 32, 33, 34, 35, 38, 39, 41	syl133anc 1205	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
43		simp22r 1075	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44		simp31r 1079	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	8, 9, 10, 11, 12, 40	lhpat2 29513	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 4, 7, 43, 22, 44, 45	syl222anc 1198	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
47	42, 46	eqeltrd 2358	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
48		simp11 985	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
49		simp12 986	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
50		simp13 987	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
51		simp31l 1078	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
52	8, 9, 10, 11, 12, 13, 14	cdleme3fa 29704	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53	48, 49, 50, 32, 51, 36, 52	syl132anc 1200	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
54	8, 9, 10, 11, 12, 13, 23	cdleme3fa 29704	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	48, 49, 50, 33, 51, 37, 54	syl132anc 1200	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
56		simp33r 1083	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
57	8, 9, 10, 11, 12, 13, 14, 23	cdleme16b 29747	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
58	31, 32, 33, 35, 36, 37, 56, 57	syl133anc 1205	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
59		eqid 2284	. . . . . . 7
60	9, 11, 59	llni2 28980	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
61	1, 53, 55, 58, 60	syl31anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
62	8, 9, 10, 11, 12, 19	cdlemeda 29766	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
63	1, 4, 7, 43, 18, 39, 36, 62	syl223anc 1208	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
64		simp23r 1077	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
65	8, 9, 10, 11, 12, 26	cdlemeda 29766	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
66	1, 4, 22, 64, 18, 39, 37, 65	syl223anc 1208	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
67		simp32 992	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
68		simp33l 1082	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
69	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20j 29786	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
70	48, 49, 50, 34, 32, 33, 35, 67, 68, 69	syl333anc 1214	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
71	9, 11, 59	llni2 28980	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
72	1, 63, 66, 70, 71	syl31anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
73		eqid 2284	. . . . . 6
74	9, 10, 11, 59, 73	2llnmj 29028	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
75	1, 61, 72, 74	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
76	47, 75	mpbid 201	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
77	30, 76	eqeltrd 2358	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
78	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20l1 29788	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	48, 49, 50, 18, 7, 43, 51, 36, 39, 78	syl333anc 1214	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80		eqid 2284	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
81	8, 9, 10, 11, 12, 13, 23, 14, 26, 19, 80	cdleme20l1 29788	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
82	48, 49, 50, 18, 22, 64, 51, 37, 39, 81	syl333anc 1214	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
83	9, 10, 11, 59, 73	2llnmj 29028	. . 3 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
84	1, 79, 82, 83	syl3anc 1182	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
85	77, 84	mpbird 223	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 176 $/\$ wa 358 $/\$ w3a 934

wceq 1623

wcel 1685

wne 2447 class class class wbr 4024

cfv 5221 (class class class)co 5820

cbs 13144

cple 13211

cjn 14074

cmee 14075

clat 14147

catm 28732

chlt 28819

clln 28959

clpl 28960

clh 29452

This theorem is referenced by: cdleme20l 29790

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1636 ax-8 1644 ax-13 1687 ax-14 1689 ax-6 1704 ax-7 1709 ax-11 1716 ax-12 1868 ax-ext 2265 ax-rep 4132 ax-sep 4142 ax-nul 4150 ax-pow 4187 ax-pr 4213 ax-un 4511

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1631 df-eu 2148 df-mo 2149 df-clab 2271 df-cleq 2277 df-clel 2280 df-nfc 2409 df-ne 2449 df-nel 2450 df-ral 2549 df-rex 2550 df-reu 2551 df-rab 2553 df-v 2791 df-sbc 2993 df-csb 3083 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3457 df-if 3567 df-pw 3628 df-sn 3647 df-pr 3648 df-op 3650 df-uni 3829 df-iun 3908 df-iin 3909 df-br 4025 df-opab 4079 df-mpt 4080 df-id 4308 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-ima 4701 df-fun 5223 df-fn 5224 df-f 5225 df-f1 5226 df-fo 5227 df-f1o 5228 df-fv 5229 df-ov 5823 df-oprab 5824 df-mpt2 5825 df-1st 6084 df-2nd 6085 df-iota 6253 df-undef 6292 df-riota 6300 df-poset 14076 df-plt 14088 df-lub 14104 df-glb 14105 df-join 14106 df-meet 14107 df-p0 14141 df-p1 14142 df-lat 14148 df-clat 14210 df-oposet 28645 df-ol 28647 df-oml 28648 df-covers 28735 df-ats 28736 df-atl 28767 df-cvlat 28791 df-hlat 28820 df-llines 28966 df-lplanes 28967 df-lvols 28968 df-lines 28969 df-psubsp 28971 df-pmap 28972 df-padd 29264 df-lhyp 29456

W3C validator