cdlemc5 - Mathbox for Norm Megill

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

Theorem cdlemc5 30689

Description: Lemma for cdlemc 30691. (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 981	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2		simp23l 1078	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
3		simp1 957	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp21 990	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		cdlemc3.l	. . . . . . 7
6		cdlemc3.a	. . . . . . 7
7		cdlemc3.h	. . . . . . 7
8		cdlemc3.t	. . . . . . 7
9	5, 6, 7, 8	ltrnat 30634	. . . . . 6 $/\$ $/\$ $/\$
10	3, 4, 2, 9	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
11		cdlemc3.j	. . . . . 6 $.\/$
12	5, 11, 6	hlatlej2 29870	. . . . 5 $/\$ $/\$ $.\/$
13	1, 2, 10, 12	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
14		simp23 992	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
15		cdlemc3.r	. . . . . 6
16	5, 11, 6, 7, 8, 15	trljat1 30660	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17	3, 4, 14, 16	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
18	13, 17	breqtrrd 4206	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19		simp22 991	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
20		cdlemc3.m	. . . . 5 $./\$
21	5, 11, 20, 6, 7, 8	cdlemc2 30686	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
22	3, 4, 19, 14, 21	syl112anc 1188	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
23		hllat 29858	. . . . 5
24	1, 23	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		eqid 2412	. . . . . . 7
26	25, 6	atbase 29784	. . . . . 6
27	2, 26	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
28	25, 7, 8	ltrncl 30619	. . . . 5 $/\$ $/\$ $/\$
29	3, 4, 27, 28	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
30	25, 7, 8, 15	trlcl 30658	. . . . . 6 $/\$ $/\$
31	3, 4, 30	syl2anc 643	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	25, 11	latjcl 14442	. . . . 5 $/\$ $/\$ $.\/$
33	24, 27, 31, 32	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34		simp22l 1076	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
35	25, 6	atbase 29784	. . . . . . 7
36	34, 35	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
37	25, 7, 8	ltrncl 30619	. . . . . 6 $/\$ $/\$ $/\$
38	3, 4, 36, 37	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
39	25, 11, 6	hlatjcl 29861	. . . . . . 7 $/\$ $/\$ $.\/$
40	1, 34, 2, 39	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		simp1r 982	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
42	25, 7	lhpbase 30492	. . . . . . 7
43	41, 42	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
44	25, 20	latmcl 14443	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
45	24, 40, 43, 44	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
46	25, 11	latjcl 14442	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
47	24, 38, 45, 46	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
48	25, 5, 20	latlem12 14470	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
49	24, 29, 33, 47, 48	syl13anc 1186	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
50	18, 22, 49	mpbi2and 888	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51		hlatl 29855	. . . 4
52	1, 51	syl 16	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp3r 986	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	5, 6, 7, 8, 15	trlat 30663	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	3, 19, 4, 53, 54	syl112anc 1188	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
56	5, 7, 8, 15	trlle 30678	. . . . . . 7 $/\$ $/\$
57	3, 4, 56	syl2anc 643	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		simp23r 1079	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
59		nbrne2 4198	. . . . . . 7 $/\$
60	59	necomd 2658	. . . . . 6 $/\$
61	57, 58, 60	syl2anc 643	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
62		eqid 2412	. . . . . 6
63	11, 6, 62	llni2 30006	. . . . 5 $/\$ $/\$ $/\$ $.\/$
64	1, 2, 55, 61, 63	syl31anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
65	5, 6, 7, 8	ltrnat 30634	. . . . . 6 $/\$ $/\$ $/\$
66	3, 4, 34, 65	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
67	5, 11, 6	hlatlej1 29869	. . . . . . . 8 $/\$ $/\$ $.\/$
68	1, 34, 66, 67	syl3anc 1184	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
69		simp3l 985	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70		nbrne2 4198	. . . . . . 7 $.\/$ $/\$ $.\/$
71	68, 69, 70	syl2anc 643	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
72	5, 11, 20, 6, 7	lhpat 30537	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
73	3, 19, 2, 71, 72	syl112anc 1188	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
74	25, 5, 20	latmle2 14469	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
75	24, 40, 43, 74	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
76	5, 6, 7, 8	ltrnel 30633	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	simprd 450	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	3, 4, 19, 77	syl3anc 1184	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
79		nbrne2 4198	. . . . . . 7 $.\/$ $./\$ $/\$ $.\/$ $./\$
80	79	necomd 2658	. . . . . 6 $.\/$ $./\$ $/\$ $.\/$ $./\$
81	75, 78, 80	syl2anc 643	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
82	11, 6, 62	llni2 30006	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
83	1, 66, 73, 81, 82	syl31anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
84	5, 11, 20, 6, 7, 8, 15	cdlemc4 30688	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
85	84	3adant3r 1181	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
86	25, 20	latmcl 14443	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
87	24, 33, 47, 86	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
88		eqid 2412	. . . . . 6
89	25, 5, 88, 6	atlen0 29805	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
90	52, 87, 10, 50, 89	syl31anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
91	20, 88, 6, 62	2llnmat 30018	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
92	1, 64, 83, 85, 90, 91	syl32anc 1192	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
93	5, 6	atcmp 29806	. . 3 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
94	52, 10, 92, 93	syl3anc 1184	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
95	50, 94	mpbid 202	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

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

wceq 1649

wcel 1721

wne 2575 class class class wbr 4180

cfv 5421 (class class class)co 6048

cbs 13432

cple 13499

cjn 14364

cmee 14365

cp0 14429

clat 14437

catm 29758

cal 29759

chlt 29845

clln 29985

clh 30478

cltrn 30595

ctrl 30652

This theorem is referenced by: cdlemc 30691

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2393 ax-rep 4288 ax-sep 4298 ax-nul 4306 ax-pow 4345 ax-pr 4371 ax-un 4668

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2266 df-mo 2267 df-clab 2399 df-cleq 2405 df-clel 2408 df-nfc 2537 df-ne 2577 df-nel 2578 df-ral 2679 df-rex 2680 df-reu 2681 df-rab 2683 df-v 2926 df-sbc 3130 df-csb 3220 df-dif 3291 df-un 3293 df-in 3295 df-ss 3302 df-nul 3597 df-if 3708 df-pw 3769 df-sn 3788 df-pr 3789 df-op 3791 df-uni 3984 df-iun 4063 df-iin 4064 df-br 4181 df-opab 4235 df-mpt 4236 df-id 4466 df-xp 4851 df-rel 4852 df-cnv 4853 df-co 4854 df-dm 4855 df-rn 4856 df-res 4857 df-ima 4858 df-iota 5385 df-fun 5423 df-fn 5424 df-f 5425 df-f1 5426 df-fo 5427 df-f1o 5428 df-fv 5429 df-ov 6051 df-oprab 6052 df-mpt2 6053 df-1st 6316 df-2nd 6317 df-undef 6510 df-riota 6516 df-map 6987 df-poset 14366 df-plt 14378 df-lub 14394 df-glb 14395 df-join 14396 df-meet 14397 df-p0 14431 df-p1 14432 df-lat 14438 df-clat 14500 df-oposet 29671 df-ol 29673 df-oml 29674 df-covers 29761 df-ats 29762 df-atl 29793 df-cvlat 29817 df-hlat 29846 df-llines 29992 df-psubsp 29997 df-pmap 29998 df-padd 30290 df-lhyp 30482 df-laut 30483 df-ldil 30598 df-ltrn 30599 df-trl 30653

W3C validator