cdlemc5 - Mathbox for Norm Megill

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

Theorem cdlemc5 31065

Description: Lemma for cdlemc 31067. (Contributed by NM, 26-May-2012.)

**Hypotheses**
Ref	Expression
cdlemc3.l
cdlemc3.j	$.\/$
cdlemc3.m	$./\$
cdlemc3.a
cdlemc3.h
cdlemc3.t
cdlemc3.r

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

**Proof of Theorem cdlemc5**
Step	Hyp	Ref	Expression
1		simp1l 982	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2		simp23l 1079	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
3		simp1 958	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp21 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		cdlemc3.l	. . . . . . 7
6		cdlemc3.a	. . . . . . 7
7		cdlemc3.h	. . . . . . 7
8		cdlemc3.t	. . . . . . 7
9	5, 6, 7, 8	ltrnat 31010	. . . . . 6 $/\$ $/\$ $/\$
10	3, 4, 2, 9	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
11		cdlemc3.j	. . . . . 6 $.\/$
12	5, 11, 6	hlatlej2 30246	. . . . 5 $/\$ $/\$ $.\/$
13	1, 2, 10, 12	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
14		simp23 993	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
15		cdlemc3.r	. . . . . 6
16	5, 11, 6, 7, 8, 15	trljat1 31036	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17	3, 4, 14, 16	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
18	13, 17	breqtrrd 4241	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19		simp22 992	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
20		cdlemc3.m	. . . . 5 $./\$
21	5, 11, 20, 6, 7, 8	cdlemc2 31062	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
22	3, 4, 19, 14, 21	syl112anc 1189	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
23		hllat 30234	. . . . 5
24	1, 23	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		eqid 2438	. . . . . . 7
26	25, 6	atbase 30160	. . . . . 6
27	2, 26	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
28	25, 7, 8	ltrncl 30995	. . . . 5 $/\$ $/\$ $/\$
29	3, 4, 27, 28	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
30	25, 7, 8, 15	trlcl 31034	. . . . . 6 $/\$ $/\$
31	3, 4, 30	syl2anc 644	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	25, 11	latjcl 14484	. . . . 5 $/\$ $/\$ $.\/$
33	24, 27, 31, 32	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34		simp22l 1077	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
35	25, 6	atbase 30160	. . . . . . 7
36	34, 35	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
37	25, 7, 8	ltrncl 30995	. . . . . 6 $/\$ $/\$ $/\$
38	3, 4, 36, 37	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
39	25, 11, 6	hlatjcl 30237	. . . . . . 7 $/\$ $/\$ $.\/$
40	1, 34, 2, 39	syl3anc 1185	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		simp1r 983	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
42	25, 7	lhpbase 30868	. . . . . . 7
43	41, 42	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
44	25, 20	latmcl 14485	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
45	24, 40, 43, 44	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
46	25, 11	latjcl 14484	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
47	24, 38, 45, 46	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
48	25, 5, 20	latlem12 14512	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
49	24, 29, 33, 47, 48	syl13anc 1187	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
50	18, 22, 49	mpbi2and 889	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51		hlatl 30231	. . . 4
52	1, 51	syl 16	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp3r 987	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	5, 6, 7, 8, 15	trlat 31039	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	3, 19, 4, 53, 54	syl112anc 1189	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
56	5, 7, 8, 15	trlle 31054	. . . . . . 7 $/\$ $/\$
57	3, 4, 56	syl2anc 644	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		simp23r 1080	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
59		nbrne2 4233	. . . . . . 7 $/\$
60	59	necomd 2689	. . . . . 6 $/\$
61	57, 58, 60	syl2anc 644	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
62		eqid 2438	. . . . . 6
63	11, 6, 62	llni2 30382	. . . . 5 $/\$ $/\$ $/\$ $.\/$
64	1, 2, 55, 61, 63	syl31anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
65	5, 6, 7, 8	ltrnat 31010	. . . . . 6 $/\$ $/\$ $/\$
66	3, 4, 34, 65	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
67	5, 11, 6	hlatlej1 30245	. . . . . . . 8 $/\$ $/\$ $.\/$
68	1, 34, 66, 67	syl3anc 1185	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
69		simp3l 986	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70		nbrne2 4233	. . . . . . 7 $.\/$ $/\$ $.\/$
71	68, 69, 70	syl2anc 644	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
72	5, 11, 20, 6, 7	lhpat 30913	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
73	3, 19, 2, 71, 72	syl112anc 1189	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
74	25, 5, 20	latmle2 14511	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
75	24, 40, 43, 74	syl3anc 1185	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
76	5, 6, 7, 8	ltrnel 31009	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	simprd 451	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	3, 4, 19, 77	syl3anc 1185	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
79		nbrne2 4233	. . . . . . 7 $.\/$ $./\$ $/\$ $.\/$ $./\$
80	79	necomd 2689	. . . . . 6 $.\/$ $./\$ $/\$ $.\/$ $./\$
81	75, 78, 80	syl2anc 644	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
82	11, 6, 62	llni2 30382	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
83	1, 66, 73, 81, 82	syl31anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
84	5, 11, 20, 6, 7, 8, 15	cdlemc4 31064	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
85	84	3adant3r 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
86	25, 20	latmcl 14485	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
87	24, 33, 47, 86	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
88		eqid 2438	. . . . . 6
89	25, 5, 88, 6	atlen0 30181	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
90	52, 87, 10, 50, 89	syl31anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
91	20, 88, 6, 62	2llnmat 30394	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
92	1, 64, 83, 85, 90, 91	syl32anc 1193	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
93	5, 6	atcmp 30182	. . 3 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
94	52, 10, 92, 93	syl3anc 1185	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
95	50, 94	mpbid 203	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

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

wceq 1653

wcel 1726

wne 2601 class class class wbr 4215

cfv 5457 (class class class)co 6084

cbs 13474

cple 13541

cjn 14406

cmee 14407

cp0 14471

clat 14479

catm 30134

cal 30135

chlt 30221

clln 30361

clh 30854

cltrn 30971

ctrl 31028

This theorem is referenced by: cdlemc 31067

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1556 ax-5 1567 ax-17 1627 ax-9 1667 ax-8 1688 ax-13 1728 ax-14 1730 ax-6 1745 ax-7 1750 ax-11 1762 ax-12 1951 ax-ext 2419 ax-rep 4323 ax-sep 4333 ax-nul 4341 ax-pow 4380 ax-pr 4406 ax-un 4704

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3an 939 df-tru 1329 df-ex 1552 df-nf 1555 df-sb 1660 df-eu 2287 df-mo 2288 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2712 df-rex 2713 df-reu 2714 df-rab 2716 df-v 2960 df-sbc 3164 df-csb 3254 df-dif 3325 df-un 3327 df-in 3329 df-ss 3336 df-nul 3631 df-if 3742 df-pw 3803 df-sn 3822 df-pr 3823 df-op 3825 df-uni 4018 df-iun 4097 df-iin 4098 df-br 4216 df-opab 4270 df-mpt 4271 df-id 4501 df-xp 4887 df-rel 4888 df-cnv 4889 df-co 4890 df-dm 4891 df-rn 4892 df-res 4893 df-ima 4894 df-iota 5421 df-fun 5459 df-fn 5460 df-f 5461 df-f1 5462 df-fo 5463 df-f1o 5464 df-fv 5465 df-ov 6087 df-oprab 6088 df-mpt2 6089 df-1st 6352 df-2nd 6353 df-undef 6546 df-riota 6552 df-map 7023 df-poset 14408 df-plt 14420 df-lub 14436 df-glb 14437 df-join 14438 df-meet 14439 df-p0 14473 df-p1 14474 df-lat 14480 df-clat 14542 df-oposet 30047 df-ol 30049 df-oml 30050 df-covers 30137 df-ats 30138 df-atl 30169 df-cvlat 30193 df-hlat 30222 df-llines 30368 df-psubsp 30373 df-pmap 30374 df-padd 30666 df-lhyp 30858 df-laut 30859 df-ldil 30974 df-ltrn 30975 df-trl 31029

W3C validator