cdleme0nex - Mathbox for Norm Megill

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

Theorem cdleme0nex 33768

Description: Part of proof of Lemma E in [Crawley] p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p $\/$ q/0 (i.e. the sublattice from 0 to p $\/$ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a 33689- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 32821, our

$.\/$

is a shorter way to express

$/\$

$.\/$

. Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012.)

**Hypotheses**
Ref	Expression
cdleme0nex.l
cdleme0nex.j	$.\/$
cdleme0nex.a

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

Distinct variable groups:

$.\/$ ,

Allowed substitution hint:

(

)

**Proof of Theorem cdleme0nex**
Step	Hyp	Ref	Expression
1		simp3r 1034	. . . 4 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simp12 1036	. . . 4 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
3	1, 2	jca 534	. . 3 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
4		simp3l 1033	. . . . . 6 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
5		simp13 1037	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
6		ralnex 2811	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
7	5, 6	sylibr 215	. . . . . 6 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
8		breq1 4369	. . . . . . . . . 10
9	8	notbid 295	. . . . . . . . 9
10		oveq2 6257	. . . . . . . . . 10 $.\/$ $.\/$
11		oveq2 6257	. . . . . . . . . 10 $.\/$ $.\/$
12	10, 11	eqeq12d 2443	. . . . . . . . 9 $.\/$ $.\/$ $.\/$ $.\/$
13	9, 12	anbi12d 715	. . . . . . . 8 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
14	13	notbid 295	. . . . . . 7 $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
15	14	rspcva 3123	. . . . . 6 $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
16	4, 7, 15	syl2anc 665	. . . . 5 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simp11 1035	. . . . . . . 8 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
18		hlcvl 32837	. . . . . . . 8
19	17, 18	syl 17	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
20		simp21 1038	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
21		simp22 1039	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
22		simp23 1040	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
23		cdleme0nex.a	. . . . . . . 8
24		cdleme0nex.l	. . . . . . . 8
25		cdleme0nex.j	. . . . . . . 8 $.\/$
26	23, 24, 25	cvlsupr2 32821	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
27	19, 20, 21, 4, 22, 26	syl131anc 1277	. . . . . 6 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
28	27	anbi2d 708	. . . . 5 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29	16, 28	mtbid 301	. . . 4 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
30		ianor 490	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $\/$ $/\$ $.\/$
31		df-3an 984	. . . . . . . 8 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$
32	31	anbi2i 698	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
33		an12 804	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
34	32, 33	bitri 252	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
35	34	notbii 297	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
36		pm4.62 420	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $\/$ $/\$ $.\/$
37	30, 35, 36	3bitr4ri 281	. . . 4 $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
38	29, 37	sylibr 215	. . 3 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
39	3, 38	mt2d 120	. 2 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
40		neanior 2693	. . 3 $/\$ $\/$
41	40	con2bii 333	. 2 $\/$ $/\$
42	39, 41	sylibr 215	1 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1872

wne 2599

wral 2714

wrex 2715 class class class wbr 4366

cfv 5544 (class class class)co 6249

cple 15140

cjn 16132

catm 32741

clc 32743

chlt 32828

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 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541

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 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-ral 2719 df-rex 2720 df-reu 2721 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-op 3948 df-uni 4163 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-id 4711 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-riota 6211 df-ov 6252 df-oprab 6253 df-preset 16116 df-poset 16134 df-plt 16147 df-lub 16163 df-glb 16164 df-join 16165 df-meet 16166 df-p0 16228 df-lat 16235 df-covers 32744 df-ats 32745 df-atl 32776 df-cvlat 32800 df-hlat 32829

This theorem is referenced by: cdleme18c 33771 cdleme18d 33773 cdlemg17b 34141 cdlemg17h 34147

W3C validator