dalem1 - Mathbox for Norm Megill

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

Theorem dalem1 32936

Description: Lemma for dath 33013. Show the lines

and

are different. (Contributed by NM, 9-Aug-2012.)

**Hypotheses**
Ref	Expression
dalema.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalemc.l
dalemc.j	$.\/$
dalemc.a
dalem1.o
dalem1.y	$.\/$ $.\/$

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

**Proof of Theorem dalem1**
Step	Hyp	Ref	Expression
1		dalema.ph	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2	1	dalemclpjs 32911	. 2 $.\/$
3	1	dalem-clpjq 32914	. . . . . 6 $.\/$
4	3	adantr 466	. . . . 5 $/\$ $.\/$ $.\/$ $.\/$
5	1	dalemkehl 32900	. . . . . . . . . 10
6	1	dalempea 32903	. . . . . . . . . 10
7	1	dalemsea 32906	. . . . . . . . . 10
8		dalemc.l	. . . . . . . . . . 11
9		dalemc.j	. . . . . . . . . . 11 $.\/$
10		dalemc.a	. . . . . . . . . . 11
11	8, 9, 10	hlatlej1 32652	. . . . . . . . . 10 $/\$ $/\$ $.\/$
12	5, 6, 7, 11	syl3anc 1264	. . . . . . . . 9 $.\/$
13	12	adantr 466	. . . . . . . 8 $/\$ $.\/$ $.\/$ $.\/$
14	1	dalemqea 32904	. . . . . . . . . . 11
15	1	dalemtea 32907	. . . . . . . . . . 11
16	8, 9, 10	hlatlej1 32652	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
17	5, 14, 15, 16	syl3anc 1264	. . . . . . . . . 10 $.\/$
18	17	adantr 466	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $.\/$
19		simpr 462	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
20	18, 19	breqtrrd 4452	. . . . . . . 8 $/\$ $.\/$ $.\/$ $.\/$
21	1	dalemkelat 32901	. . . . . . . . . 10
22	1, 10	dalempeb 32916	. . . . . . . . . 10
23	1, 10	dalemqeb 32917	. . . . . . . . . 10
24		eqid 2429	. . . . . . . . . . . 12
25	24, 9, 10	hlatjcl 32644	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
26	5, 6, 7, 25	syl3anc 1264	. . . . . . . . . 10 $.\/$
27	24, 8, 9	latjle12 16259	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
28	21, 22, 23, 26, 27	syl13anc 1266	. . . . . . . . 9 $.\/$ $/\$ $.\/$ $.\/$ $.\/$
29	28	adantr 466	. . . . . . . 8 $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
30	13, 20, 29	mpbi2and 929	. . . . . . 7 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
31	1	dalemrea 32905	. . . . . . . . . 10
32	1	dalemyeo 32909	. . . . . . . . . 10
33		dalem1.o	. . . . . . . . . . 11
34		dalem1.y	. . . . . . . . . . 11 $.\/$ $.\/$
35	9, 10, 33, 34	lplnri1 32830	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
36	5, 6, 14, 31, 32, 35	syl131anc 1277	. . . . . . . . 9
37	8, 9, 10	ps-1 32754	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
38	5, 6, 14, 36, 6, 7, 37	syl132anc 1282	. . . . . . . 8 $.\/$ $.\/$ $.\/$ $.\/$
39	38	adantr 466	. . . . . . 7 $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
40	30, 39	mpbid 213	. . . . . 6 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
41	40	breq2d 4438	. . . . 5 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
42	4, 41	mtbid 301	. . . 4 $/\$ $.\/$ $.\/$ $.\/$
43	42	ex 435	. . 3 $.\/$ $.\/$ $.\/$
44	43	necon2ad 2644	. 2 $.\/$ $.\/$ $.\/$
45	2, 44	mpd 15	1 $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1870

wne 2625 class class class wbr 4426

cfv 5601 (class class class)co 6305

cbs 15084

cple 15159

cjn 16140

clat 16242

catm 32541

chlt 32628

clpl 32769

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 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 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-ral 2787 df-rex 2788 df-reu 2789 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-op 4009 df-uni 4223 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-id 4769 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 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-preset 16124 df-poset 16142 df-plt 16155 df-lub 16171 df-glb 16172 df-join 16173 df-meet 16174 df-p0 16236 df-lat 16243 df-clat 16305 df-oposet 32454 df-ol 32456 df-oml 32457 df-covers 32544 df-ats 32545 df-atl 32576 df-cvlat 32600 df-hlat 32629 df-llines 32775 df-lplanes 32776

This theorem is referenced by: dalemcea 32937 dalem2 32938

W3C validator