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 34197

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 2422	. 2
2		cdlemg12.l	. 2
3		simp1l 1029	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
4		hllat 32898	. . 3
5	3, 4	syl 17	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
6		simp1 1005	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
7		simp3l 1033	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8		simp2ll 1072	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
9		cdlemg12.a	. . . . 5
10		cdlemg12.h	. . . . 5
11		cdlemg12.t	. . . . 5
12	2, 9, 10, 11	ltrnat 33674	. . . 4 $/\$ $/\$ $/\$
13	6, 7, 8, 12	syl3anc 1264	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
14	1, 9	atbase 32824	. . 3
15	13, 14	syl 17	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16		cdlemg12.j	. . . 4 $.\/$
17	1, 16, 9	hlatjcl 32901	. . 3 $/\$ $/\$ $.\/$
18	3, 8, 13, 17	syl3anc 1264	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
19		simp2rl 1074	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	1, 16, 9	hlatjcl 32901	. . 3 $/\$ $/\$ $.\/$
21	3, 8, 19, 20	syl3anc 1264	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
22	2, 16, 9	hlatlej2 32910	. . 3 $/\$ $/\$ $.\/$
23	3, 8, 13, 22	syl3anc 1264	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simp2l 1031	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		cdlemg12.m	. . . . 5 $./\$
26		eqid 2422	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
27	2, 16, 25, 9, 10, 26	cdleme0cp 33749	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
28	6, 24, 13, 27	syl12anc 1262	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
29	2, 16, 9	hlatlej1 32909	. . . . 5 $/\$ $/\$ $.\/$
30	3, 8, 19, 29	syl3anc 1264	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31		cdlemg12b.r	. . . . . . 7
32	2, 16, 25, 9, 10, 11, 31	trlval2 33698	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	6, 7, 24, 32	syl3anc 1264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
34		simp3r 1034	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
35	33, 34	eqbrtrrd 4446	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36	1, 9	atbase 32824	. . . . . 6
37	8, 36	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
38		simp1r 1030	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
39	1, 10	lhpbase 33532	. . . . . . 7
40	38, 39	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 25	latmcl 16297	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
42	5, 18, 40, 41	syl3anc 1264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
43	1, 2, 16	latjle12 16307	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
44	5, 37, 42, 21, 43	syl13anc 1266	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
45	30, 35, 44	mpbi2and 929	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
46	28, 45	eqbrtrrd 4446	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
47	1, 2, 5, 15, 18, 21, 23, 46	lattrd 16303	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1872 class class class wbr 4423

cfv 5601 (class class class)co 6305

cbs 15120

cple 15196

cjn 16188

cmee 16189

clat 16290

catm 32798

chlt 32885

clh 33518

cltrn 33635

ctrl 33693

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2057 ax-ext 2401 ax-rep 4536 ax-sep 4546 ax-nul 4555 ax-pow 4602 ax-pr 4660 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2273 df-mo 2274 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2568 df-ne 2616 df-ral 2776 df-rex 2777 df-reu 2778 df-rab 2780 df-v 3082 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3912 df-pw 3983 df-sn 3999 df-pr 4001 df-op 4005 df-uni 4220 df-iun 4301 df-iin 4302 df-br 4424 df-opab 4483 df-mpt 4484 df-id 4768 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-1st 6807 df-2nd 6808 df-map 7485 df-preset 16172 df-poset 16190 df-plt 16203 df-lub 16219 df-glb 16220 df-join 16221 df-meet 16222 df-p0 16284 df-p1 16285 df-lat 16291 df-clat 16353 df-oposet 32711 df-ol 32713 df-oml 32714 df-covers 32801 df-ats 32802 df-atl 32833 df-cvlat 32857 df-hlat 32886 df-psubsp 33037 df-pmap 33038 df-padd 33330 df-lhyp 33522 df-laut 33523 df-ldil 33638 df-ltrn 33639 df-trl 33694

This theorem is referenced by: cdlemg17b 34198

W3C validator