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 30384

Description: Lemma for cdlemc 30386. (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 979	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2		simp23l 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
3		simp1 955	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
4		simp21 988	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
5		cdlemc3.l	. . . . . . 7
6		cdlemc3.a	. . . . . . 7
7		cdlemc3.h	. . . . . . 7
8		cdlemc3.t	. . . . . . 7
9	5, 6, 7, 8	ltrnat 30329	. . . . . 6 $/\$ $/\$ $/\$
10	3, 4, 2, 9	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
11		cdlemc3.j	. . . . . 6 $.\/$
12	5, 11, 6	hlatlej2 29565	. . . . 5 $/\$ $/\$ $.\/$
13	1, 2, 10, 12	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
14		simp23 990	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
15		cdlemc3.r	. . . . . 6
16	5, 11, 6, 7, 8, 15	trljat1 30355	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17	3, 4, 14, 16	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
18	13, 17	breqtrrd 4049	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19		simp22 989	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
20		cdlemc3.m	. . . . 5 $./\$
21	5, 11, 20, 6, 7, 8	cdlemc2 30381	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
22	3, 4, 19, 14, 21	syl112anc 1186	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
23		hllat 29553	. . . . 5
24	1, 23	syl 15	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		eqid 2283	. . . . . . 7
26	25, 6	atbase 29479	. . . . . 6
27	2, 26	syl 15	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
28	25, 7, 8	ltrncl 30314	. . . . 5 $/\$ $/\$ $/\$
29	3, 4, 27, 28	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
30	25, 7, 8, 15	trlcl 30353	. . . . . 6 $/\$ $/\$
31	3, 4, 30	syl2anc 642	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	25, 11	latjcl 14156	. . . . 5 $/\$ $/\$ $.\/$
33	24, 27, 31, 32	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
34		simp22l 1074	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
35	25, 6	atbase 29479	. . . . . . 7
36	34, 35	syl 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
37	25, 7, 8	ltrncl 30314	. . . . . 6 $/\$ $/\$ $/\$
38	3, 4, 36, 37	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
39	25, 11, 6	hlatjcl 29556	. . . . . . 7 $/\$ $/\$ $.\/$
40	1, 34, 2, 39	syl3anc 1182	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41		simp1r 980	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
42	25, 7	lhpbase 30187	. . . . . . 7
43	41, 42	syl 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
44	25, 20	latmcl 14157	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
45	24, 40, 43, 44	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
46	25, 11	latjcl 14156	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
47	24, 38, 45, 46	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
48	25, 5, 20	latlem12 14184	. . . 4 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
49	24, 29, 33, 47, 48	syl13anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
50	18, 22, 49	mpbi2and 887	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
51		hlatl 29550	. . . 4
52	1, 51	syl 15	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp3r 984	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	5, 6, 7, 8, 15	trlat 30358	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$
55	3, 19, 4, 53, 54	syl112anc 1186	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
56	5, 7, 8, 15	trlle 30373	. . . . . . 7 $/\$ $/\$
57	3, 4, 56	syl2anc 642	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		simp23r 1077	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
59		nbrne2 4041	. . . . . . 7 $/\$
60	59	necomd 2529	. . . . . 6 $/\$
61	57, 58, 60	syl2anc 642	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
62		eqid 2283	. . . . . 6
63	11, 6, 62	llni2 29701	. . . . 5 $/\$ $/\$ $/\$ $.\/$
64	1, 2, 55, 61, 63	syl31anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
65	5, 6, 7, 8	ltrnat 30329	. . . . . 6 $/\$ $/\$ $/\$
66	3, 4, 34, 65	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
67	5, 11, 6	hlatlej1 29564	. . . . . . . 8 $/\$ $/\$ $.\/$
68	1, 34, 66, 67	syl3anc 1182	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
69		simp3l 983	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
70		nbrne2 4041	. . . . . . 7 $.\/$ $/\$ $.\/$
71	68, 69, 70	syl2anc 642	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
72	5, 11, 20, 6, 7	lhpat 30232	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
73	3, 19, 2, 71, 72	syl112anc 1186	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
74	25, 5, 20	latmle2 14183	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $./\$
75	24, 40, 43, 74	syl3anc 1182	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
76	5, 6, 7, 8	ltrnel 30328	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
77	76	simprd 449	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
78	3, 4, 19, 77	syl3anc 1182	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
79		nbrne2 4041	. . . . . . 7 $.\/$ $./\$ $/\$ $.\/$ $./\$
80	79	necomd 2529	. . . . . 6 $.\/$ $./\$ $/\$ $.\/$ $./\$
81	75, 78, 80	syl2anc 642	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$
82	11, 6, 62	llni2 29701	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
83	1, 66, 73, 81, 82	syl31anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$
84	5, 11, 20, 6, 7, 8, 15	cdlemc4 30383	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$
85	84	3adant3r 1179	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$
86	25, 20	latmcl 14157	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
87	24, 33, 47, 86	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
88		eqid 2283	. . . . . 6
89	25, 5, 88, 6	atlen0 29500	. . . . 5 $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
90	52, 87, 10, 50, 89	syl31anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
91	20, 88, 6, 62	2llnmat 29713	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
92	1, 64, 83, 85, 90, 91	syl32anc 1190	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
93	5, 6	atcmp 29501	. . 3 $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
94	52, 10, 92, 93	syl3anc 1182	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$
95	50, 94	mpbid 201	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

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

wceq 1623

wcel 1684

wne 2446 class class class wbr 4023

cfv 5255 (class class class)co 5858

cbs 13148

cple 13215

cjn 14078

cmee 14079

cp0 14143

clat 14151

catm 29453

cal 29454

chlt 29540

clln 29680

clh 30173

cltrn 30290

ctrl 30347

This theorem is referenced by: cdlemc 30386

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 1635 ax-8 1643 ax-13 1686 ax-14 1688 ax-6 1703 ax-7 1708 ax-11 1715 ax-12 1866 ax-ext 2264 ax-rep 4131 ax-sep 4141 ax-nul 4149 ax-pow 4188 ax-pr 4214 ax-un 4512

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1630 df-eu 2147 df-mo 2148 df-clab 2270 df-cleq 2276 df-clel 2279 df-nfc 2408 df-ne 2448 df-nel 2449 df-ral 2548 df-rex 2549 df-reu 2550 df-rab 2552 df-v 2790 df-sbc 2992 df-csb 3082 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3456 df-if 3566 df-pw 3627 df-sn 3646 df-pr 3647 df-op 3649 df-uni 3828 df-iun 3907 df-iin 3908 df-br 4024 df-opab 4078 df-mpt 4079 df-id 4309 df-xp 4695 df-rel 4696 df-cnv 4697 df-co 4698 df-dm 4699 df-rn 4700 df-res 4701 df-ima 4702 df-iota 5219 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-ov 5861 df-oprab 5862 df-mpt2 5863 df-1st 6122 df-2nd 6123 df-undef 6298 df-riota 6304 df-map 6774 df-poset 14080 df-plt 14092 df-lub 14108 df-glb 14109 df-join 14110 df-meet 14111 df-p0 14145 df-p1 14146 df-lat 14152 df-clat 14214 df-oposet 29366 df-ol 29368 df-oml 29369 df-covers 29456 df-ats 29457 df-atl 29488 df-cvlat 29512 df-hlat 29541 df-llines 29687 df-psubsp 29692 df-pmap 29693 df-padd 29985 df-lhyp 30177 df-laut 30178 df-ldil 30293 df-ltrn 30294 df-trl 30348

W3C validator