cdlemg17a - Mathbox for Norm Megill

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

Theorem cdlemg17a 36839

Description: TODO: FIX COMMENT (Contributed by NM, 8-May-2013.)

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

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

**Proof of Theorem cdlemg17a**
Step	Hyp	Ref	Expression
1		eqid 2396	. 2
2		cdlemg12.l	. 2
3		simp1l 1018	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
4		hllat 35540	. . 3
5	3, 4	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
6		simp1 994	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
7		simp3l 1022	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8		simp2ll 1061	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
9		cdlemg12.a	. . . . 5
10		cdlemg12.h	. . . . 5
11		cdlemg12.t	. . . . 5
12	2, 9, 10, 11	ltrnat 36316	. . . 4 $/\$ $/\$ $/\$
13	6, 7, 8, 12	syl3anc 1226	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
14	1, 9	atbase 35466	. . 3
15	13, 14	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16		cdlemg12.j	. . . 4 $.\/$
17	1, 16, 9	hlatjcl 35543	. . 3 $/\$ $/\$ $.\/$
18	3, 8, 13, 17	syl3anc 1226	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
19		simp2rl 1063	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	1, 16, 9	hlatjcl 35543	. . 3 $/\$ $/\$ $.\/$
21	3, 8, 19, 20	syl3anc 1226	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
22	2, 16, 9	hlatlej2 35552	. . 3 $/\$ $/\$ $.\/$
23	3, 8, 13, 22	syl3anc 1226	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simp2l 1020	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		cdlemg12.m	. . . . 5 $./\$
26		eqid 2396	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
27	2, 16, 25, 9, 10, 26	cdleme0cp 36391	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
28	6, 24, 13, 27	syl12anc 1224	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
29	2, 16, 9	hlatlej1 35551	. . . . 5 $/\$ $/\$ $.\/$
30	3, 8, 19, 29	syl3anc 1226	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31		cdlemg12b.r	. . . . . . 7
32	2, 16, 25, 9, 10, 11, 31	trlval2 36340	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	6, 7, 24, 32	syl3anc 1226	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
34		simp3r 1023	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
35	33, 34	eqbrtrrd 4406	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36	1, 9	atbase 35466	. . . . . 6
37	8, 36	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
38		simp1r 1019	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
39	1, 10	lhpbase 36174	. . . . . . 7
40	38, 39	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 25	latmcl 15822	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
42	5, 18, 40, 41	syl3anc 1226	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
43	1, 2, 16	latjle12 15832	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
44	5, 37, 42, 21, 43	syl13anc 1228	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
45	30, 35, 44	mpbi2and 919	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
46	28, 45	eqbrtrrd 4406	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
47	1, 2, 5, 15, 18, 21, 23, 46	lattrd 15828	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wceq 1399

wcel 1836 class class class wbr 4384

cfv 5513 (class class class)co 6218

cbs 14657

cple 14732

cjn 15713

cmee 15714

clat 15815

catm 35440

chlt 35527

clh 36160

cltrn 36277

ctrl 36335

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1633 ax-4 1646 ax-5 1719 ax-6 1765 ax-7 1808 ax-8 1838 ax-9 1840 ax-10 1855 ax-11 1860 ax-12 1872 ax-13 2020 ax-ext 2374 ax-rep 4495 ax-sep 4505 ax-nul 4513 ax-pow 4560 ax-pr 4618 ax-un 6513

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 973 df-tru 1402 df-ex 1628 df-nf 1632 df-sb 1758 df-eu 2236 df-mo 2237 df-clab 2382 df-cleq 2388 df-clel 2391 df-nfc 2546 df-ne 2593 df-ral 2751 df-rex 2752 df-reu 2753 df-rab 2755 df-v 3053 df-sbc 3270 df-csb 3366 df-dif 3409 df-un 3411 df-in 3413 df-ss 3420 df-nul 3729 df-if 3875 df-pw 3946 df-sn 3962 df-pr 3964 df-op 3968 df-uni 4181 df-iun 4262 df-iin 4263 df-br 4385 df-opab 4443 df-mpt 4444 df-id 4726 df-xp 4936 df-rel 4937 df-cnv 4938 df-co 4939 df-dm 4940 df-rn 4941 df-res 4942 df-ima 4943 df-iota 5477 df-fun 5515 df-fn 5516 df-f 5517 df-f1 5518 df-fo 5519 df-f1o 5520 df-fv 5521 df-riota 6180 df-ov 6221 df-oprab 6222 df-mpt2 6223 df-1st 6721 df-2nd 6722 df-map 7362 df-preset 15697 df-poset 15715 df-plt 15728 df-lub 15744 df-glb 15745 df-join 15746 df-meet 15747 df-p0 15809 df-p1 15810 df-lat 15816 df-clat 15878 df-oposet 35353 df-ol 35355 df-oml 35356 df-covers 35443 df-ats 35444 df-atl 35475 df-cvlat 35499 df-hlat 35528 df-psubsp 35679 df-pmap 35680 df-padd 35972 df-lhyp 36164 df-laut 36165 df-ldil 36280 df-ltrn 36281 df-trl 36336

This theorem is referenced by: cdlemg17b 36840

W3C validator