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 29760

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 1071	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		hllat 28803	. . . . 5
3	1, 2	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp11r 1072	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		simp12l 1073	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		simp13l 1075	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
7		simp22l 1079	. . . . 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 2258	. . . . . 6
16	8, 9, 10, 11, 12, 13, 14, 15	cdleme1b 29665	. . . . 5 $/\$ $/\$ $/\$ $/\$
17	1, 4, 5, 6, 7, 16	syl23anc 1194	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
18		simp21l 1077	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
19		cdleme19.d	. . . . . 6 $.\/$ $./\$
20	8, 9, 10, 11, 12, 19, 15	cdlemedb 29736	. . . . 5 $/\$ $/\$ $/\$
21	1, 4, 18, 7, 20	syl22anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
22		simp23l 1081	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
23		cdleme19.g	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
24	8, 9, 10, 11, 12, 13, 23, 15	cdleme1b 29665	. . . . 5 $/\$ $/\$ $/\$ $/\$
25	1, 4, 5, 6, 22, 24	syl23anc 1194	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
26		cdleme19.y	. . . . . 6 $.\/$ $./\$
27	8, 9, 10, 11, 12, 26, 15	cdlemedb 29736	. . . . 5 $/\$ $/\$ $/\$
28	1, 4, 18, 22, 27	syl22anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
29	15, 9	latj4 14170	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
30	3, 17, 21, 25, 28, 29	syl122anc 1196	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31		simp1 960	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
32		simp22 994	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
33		simp23 995	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
34		simp21 993	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
35		simp31 996	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
36		simp321 1110	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simp322 1111	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
38	36, 37	jca 520	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
39		simp323 1112	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40		cdleme20.v	. . . . . . 7 $.\/$ $./\$
41	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20d 29751	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42	31, 32, 33, 34, 35, 38, 39, 41	syl133anc 1210	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
43		simp22r 1080	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44		simp31r 1084	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
45	8, 9, 10, 11, 12, 40	lhpat2 29484	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
46	1, 4, 7, 43, 22, 44, 45	syl222anc 1203	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
47	42, 46	eqeltrd 2332	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
48		simp11 990	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
49		simp12 991	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
50		simp13 992	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$
51		simp31l 1083	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
52	8, 9, 10, 11, 12, 13, 14	cdleme3fa 29675	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53	48, 49, 50, 32, 51, 36, 52	syl132anc 1205	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
54	8, 9, 10, 11, 12, 13, 23	cdleme3fa 29675	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	48, 49, 50, 33, 51, 37, 54	syl132anc 1205	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
56		simp33r 1088	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
57	8, 9, 10, 11, 12, 13, 14, 23	cdleme16b 29718	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
58	31, 32, 33, 35, 36, 37, 56, 57	syl133anc 1210	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
59		eqid 2258	. . . . . . 7
60	9, 11, 59	llni2 28951	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
61	1, 53, 55, 58, 60	syl31anc 1190	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
62	8, 9, 10, 11, 12, 19	cdlemeda 29737	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
63	1, 4, 7, 43, 18, 39, 36, 62	syl223anc 1213	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
64		simp23r 1082	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
65	8, 9, 10, 11, 12, 26	cdlemeda 29737	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
66	1, 4, 22, 64, 18, 39, 37, 65	syl223anc 1213	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
67		simp32 997	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
68		simp33l 1087	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
69	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20j 29757	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
70	48, 49, 50, 34, 32, 33, 35, 67, 68, 69	syl333anc 1219	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
71	9, 11, 59	llni2 28951	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
72	1, 63, 66, 70, 71	syl31anc 1190	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
73		eqid 2258	. . . . . 6
74	9, 10, 11, 59, 73	2llnmj 28999	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
75	1, 61, 72, 74	syl3anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
76	47, 75	mpbid 203	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
77	30, 76	eqeltrd 2332	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
78	8, 9, 10, 11, 12, 13, 14, 23, 19, 26, 40	cdleme20l1 29759	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	48, 49, 50, 18, 7, 43, 51, 36, 39, 78	syl333anc 1219	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
80		eqid 2258	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
81	8, 9, 10, 11, 12, 13, 23, 14, 26, 19, 80	cdleme20l1 29759	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
82	48, 49, 50, 18, 22, 64, 51, 37, 39, 81	syl333anc 1219	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
83	9, 10, 11, 59, 73	2llnmj 28999	. . 3 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
84	1, 79, 82, 83	syl3anc 1187	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $.\/$
85	77, 84	mpbird 225	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 5

wi 6

wb 178 $/\$ wa 360 $/\$ w3a 939

wceq 1619

wcel 1621

wne 2421 class class class wbr 3997

cfv 4673 (class class class)co 5792

cbs 13111

cple 13178

cjn 14041

cmee 14042

clat 14114

catm 28703

chlt 28790

clln 28930

clpl 28931

clh 29423

This theorem is referenced by: cdleme20l 29761

This theorem was proved from axioms: ax-1 7 ax-2 8 ax-3 9 ax-mp 10 ax-5 1533 ax-6 1534 ax-7 1535 ax-gen 1536 ax-8 1623 ax-11 1624 ax-13 1625 ax-14 1626 ax-17 1628 ax-12o 1664 ax-10 1678 ax-9 1684 ax-4 1692 ax-16 1927 ax-ext 2239 ax-rep 4105 ax-sep 4115 ax-nul 4123 ax-pow 4160 ax-pr 4186 ax-un 4484

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3or 940 df-3an 941 df-tru 1315 df-ex 1538 df-nf 1540 df-sb 1884 df-eu 2122 df-mo 2123 df-clab 2245 df-cleq 2251 df-clel 2254 df-nfc 2383 df-ne 2423 df-nel 2424 df-ral 2523 df-rex 2524 df-reu 2525 df-rab 2527 df-v 2765 df-sbc 2967 df-csb 3057 df-dif 3130 df-un 3132 df-in 3134 df-ss 3141 df-nul 3431 df-if 3540 df-pw 3601 df-sn 3620 df-pr 3621 df-op 3623 df-uni 3802 df-iun 3881 df-iin 3882 df-br 3998 df-opab 4052 df-mpt 4053 df-id 4281 df-xp 4675 df-rel 4676 df-cnv 4677 df-co 4678 df-dm 4679 df-rn 4680 df-res 4681 df-ima 4682 df-fun 4683 df-fn 4684 df-f 4685 df-f1 4686 df-fo 4687 df-f1o 4688 df-fv 4689 df-ov 5795 df-oprab 5796 df-mpt2 5797 df-1st 6056 df-2nd 6057 df-iota 6225 df-undef 6264 df-riota 6272 df-poset 14043 df-plt 14055 df-lub 14071 df-glb 14072 df-join 14073 df-meet 14074 df-p0 14108 df-p1 14109 df-lat 14115 df-clat 14177 df-oposet 28616 df-ol 28618 df-oml 28619 df-covers 28706 df-ats 28707 df-atl 28738 df-cvlat 28762 df-hlat 28791 df-llines 28937 df-lplanes 28938 df-lvols 28939 df-lines 28940 df-psubsp 28942 df-pmap 28943 df-padd 29235 df-lhyp 29427

W3C validator