cdleme22b - Mathbox for Norm Megill

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

Theorem cdleme22b 33825

Description: Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t $\/$ v =/= p $\/$ q and s

p $\/$ q implies

p $\/$ q. (Contributed by NM, 2-Dec-2012.)

**Hypotheses**
Ref	Expression
cdleme22.l
cdleme22.j	$.\/$
cdleme22.m	$./\$
cdleme22.a
cdleme22.h

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

**Proof of Theorem cdleme22b**
Step	Hyp	Ref	Expression
1		simp1l 1012	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp1r1 1084	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3		simp1r2 1085	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		simp1r3 1086	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
5		cdleme22.j	. . . . . . 7 $.\/$
6		cdleme22.a	. . . . . . 7
7		eqid 2438	. . . . . . 7
8	5, 6, 7	llni2 32996	. . . . . 6 $/\$ $/\$ $/\$ $.\/$
9	1, 2, 3, 4, 8	syl31anc 1221	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10	6, 7	llnneat 32998	. . . . 5 $/\$ $.\/$ $.\/$
11	1, 9, 10	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
12		eqid 2438	. . . . . 6
13	12, 7	llnn0 33000	. . . . 5 $/\$ $.\/$ $.\/$
14	1, 9, 13	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
15	11, 14	jca 532	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
16		df-ne 2603	. . . . 5 $.\/$ $.\/$
17	16	anbi2i 694	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
18		pm4.56 495	. . . 4 $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
19	17, 18	bitri 249	. . 3 $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
20	15, 19	sylib 196	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $\/$ $.\/$
21		simp3r2 1097	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
22		simp3l 1016	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
23		cdleme22.l	. . . . . . . . 9
24	23, 5, 6	hlatlej1 32859	. . . . . . . 8 $/\$ $/\$ $.\/$
25	1, 3, 22, 24	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
26		hllat 32848	. . . . . . . . 9
27	1, 26	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
28		eqid 2438	. . . . . . . . . 10
29	28, 6	atbase 32774	. . . . . . . . 9
30	2, 29	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
31	28, 6	atbase 32774	. . . . . . . . 9
32	3, 31	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
33	28, 5, 6	hlatjcl 32851	. . . . . . . . 9 $/\$ $/\$ $.\/$
34	1, 3, 22, 33	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
35	28, 23, 5	latjle12 15224	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
36	27, 30, 32, 34, 35	syl13anc 1220	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
37	21, 25, 36	mpbi2and 912	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
38	37	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
39		simp3r3 1098	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
40	39	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
41		simpr 461	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
42		simp21 1021	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
43		simp22 1022	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
44	28, 5, 6	hlatjcl 32851	. . . . . . . . 9 $/\$ $/\$ $.\/$
45	1, 42, 43, 44	syl3anc 1218	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46	28, 23, 5	latjle12 15224	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
47	27, 30, 32, 45, 46	syl13anc 1220	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	47	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
49	40, 41, 48	mpbi2and 912	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
50	28, 5, 6	hlatjcl 32851	. . . . . . . 8 $/\$ $/\$ $.\/$
51	1, 2, 3, 50	syl3anc 1218	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
52		cdleme22.m	. . . . . . . 8 $./\$
53	28, 23, 52	latlem12 15240	. . . . . . 7 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
54	27, 51, 34, 45, 53	syl13anc 1220	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
55	54	adantr 465	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
56	38, 49, 55	mpbi2and 912	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
57	56	ex 434	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
58		hlop 32847	. . . . . . . 8
59	1, 58	syl 16	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
60	59	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
61	51	adantr 465	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
62		simprl 755	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
63		simprr 756	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
64	28, 23, 12, 6	leat3 32780	. . . . . 6 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
65	60, 61, 62, 63, 64	syl31anc 1221	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
66	65	exp32 605	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
67		breq2 4291	. . . . . . . . 9 $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
68	67	biimpa 484	. . . . . . . 8 $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
69	28, 23, 12	ople0 32672	. . . . . . . . 9 $/\$ $.\/$ $.\/$ $.\/$
70	59, 51, 69	syl2anc 661	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
71	68, 70	syl5ib 219	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
72	71	imp 429	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$
73	72	olcd 393	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
74	73	exp32 605	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
75		simp3r1 1096	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
76	5, 52, 12, 6	2atmat0 33010	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $\/$ $.\/$ $./\$ $.\/$
77	1, 3, 22, 42, 43, 75, 76	syl33anc 1233	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $\/$ $.\/$ $./\$ $.\/$
78	66, 74, 77	mpjaod 381	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $\/$ $.\/$
79	57, 78	syld 44	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $\/$ $.\/$
80	20, 79	mtod 177	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1369

wcel 1756

wne 2601 class class class wbr 4287

cfv 5413 (class class class)co 6086

cbs 14166

cple 14237

cjn 15106

cmee 15107

cp0 15199

clat 15207

cops 32657

catm 32748

chlt 32835

clln 32975

clh 33468

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-ral 2715 df-rex 2716 df-reu 2717 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-p1 15202 df-lat 15208 df-clat 15270 df-oposet 32661 df-ol 32663 df-oml 32664 df-covers 32751 df-ats 32752 df-atl 32783 df-cvlat 32807 df-hlat 32836 df-llines 32982

This theorem is referenced by: cdleme22cN 33826 cdleme27a 33851

W3C validator