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 34644

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 2454	. 2
2		cdlemg12.l	. 2
3		simp1l 1012	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
4		hllat 33347	. . 3
5	3, 4	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
6		simp1 988	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
7		simp3l 1016	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
8		simp2ll 1055	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
9		cdlemg12.a	. . . . 5
10		cdlemg12.h	. . . . 5
11		cdlemg12.t	. . . . 5
12	2, 9, 10, 11	ltrnat 34123	. . . 4 $/\$ $/\$ $/\$
13	6, 7, 8, 12	syl3anc 1219	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
14	1, 9	atbase 33273	. . 3
15	13, 14	syl 16	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16		cdlemg12.j	. . . 4 $.\/$
17	1, 16, 9	hlatjcl 33350	. . 3 $/\$ $/\$ $.\/$
18	3, 8, 13, 17	syl3anc 1219	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
19		simp2rl 1057	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	1, 16, 9	hlatjcl 33350	. . 3 $/\$ $/\$ $.\/$
21	3, 8, 19, 20	syl3anc 1219	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
22	2, 16, 9	hlatlej2 33359	. . 3 $/\$ $/\$ $.\/$
23	3, 8, 13, 22	syl3anc 1219	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simp2l 1014	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		cdlemg12.m	. . . . 5 $./\$
26		eqid 2454	. . . . 5 $.\/$ $./\$ $.\/$ $./\$
27	2, 16, 25, 9, 10, 26	cdleme0cp 34197	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
28	6, 24, 13, 27	syl12anc 1217	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
29	2, 16, 9	hlatlej1 33358	. . . . 5 $/\$ $/\$ $.\/$
30	3, 8, 19, 29	syl3anc 1219	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31		cdlemg12b.r	. . . . . . 7
32	2, 16, 25, 9, 10, 11, 31	trlval2 34146	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$
33	6, 7, 24, 32	syl3anc 1219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
34		simp3r 1017	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
35	33, 34	eqbrtrrd 4423	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
36	1, 9	atbase 33273	. . . . . 6
37	8, 36	syl 16	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
38		simp1r 1013	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
39	1, 10	lhpbase 33981	. . . . . . 7
40	38, 39	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
41	1, 25	latmcl 15342	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$
42	5, 18, 40, 41	syl3anc 1219	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$
43	1, 2, 16	latjle12 15352	. . . . 5 $/\$ $/\$ $.\/$ $./\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
44	5, 37, 42, 21, 43	syl13anc 1221	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
45	30, 35, 44	mpbi2and 912	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
46	28, 45	eqbrtrrd 4423	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
47	1, 2, 5, 15, 18, 21, 23, 46	lattrd 15348	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758 class class class wbr 4401

cfv 5527 (class class class)co 6201

cbs 14293

cple 14365

cjn 15234

cmee 15235

clat 15335

catm 33247

chlt 33334

clh 33967

cltrn 34084

ctrl 34141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1955 ax-ext 2432 ax-rep 4512 ax-sep 4522 ax-nul 4530 ax-pow 4579 ax-pr 4640 ax-un 6483

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2266 df-mo 2267 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2650 df-ral 2804 df-rex 2805 df-reu 2806 df-rab 2808 df-v 3080 df-sbc 3295 df-csb 3397 df-dif 3440 df-un 3442 df-in 3444 df-ss 3451 df-nul 3747 df-if 3901 df-pw 3971 df-sn 3987 df-pr 3989 df-op 3993 df-uni 4201 df-iun 4282 df-iin 4283 df-br 4402 df-opab 4460 df-mpt 4461 df-id 4745 df-xp 4955 df-rel 4956 df-cnv 4957 df-co 4958 df-dm 4959 df-rn 4960 df-res 4961 df-ima 4962 df-iota 5490 df-fun 5529 df-fn 5530 df-f 5531 df-f1 5532 df-fo 5533 df-f1o 5534 df-fv 5535 df-riota 6162 df-ov 6204 df-oprab 6205 df-mpt2 6206 df-1st 6688 df-2nd 6689 df-map 7327 df-poset 15236 df-plt 15248 df-lub 15264 df-glb 15265 df-join 15266 df-meet 15267 df-p0 15329 df-p1 15330 df-lat 15336 df-clat 15398 df-oposet 33160 df-ol 33162 df-oml 33163 df-covers 33250 df-ats 33251 df-atl 33282 df-cvlat 33306 df-hlat 33335 df-psubsp 33486 df-pmap 33487 df-padd 33779 df-lhyp 33971 df-laut 33972 df-ldil 34087 df-ltrn 34088 df-trl 34142

This theorem is referenced by: cdlemg17b 34645

W3C validator