cdlemg42 - Mathbox for Norm Megill

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

Theorem cdlemg42 34208

Description: Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.)

**Hypotheses**
Ref	Expression
cdlemg42.l
cdlemg42.j	$.\/$
cdlemg42.a
cdlemg42.h
cdlemg42.t
cdlemg42.r

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

**Proof of Theorem cdlemg42**
Step	Hyp	Ref	Expression
1		simp33 1043	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
2		simpl1l 1056	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
3		simp31l 1128	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
4	3	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
5		simp1 1005	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
6		simp2l 1031	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
7		cdlemg42.l	. . . . . . . . . . . 12
8		cdlemg42.a	. . . . . . . . . . . 12
9		cdlemg42.h	. . . . . . . . . . . 12
10		cdlemg42.t	. . . . . . . . . . . 12
11	7, 8, 9, 10	ltrnat 33617	. . . . . . . . . . 11 $/\$ $/\$ $/\$
12	5, 6, 3, 11	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
13	12	adantr 466	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
14		cdlemg42.j	. . . . . . . . . 10 $.\/$
15	7, 14, 8	hlatlej1 32852	. . . . . . . . 9 $/\$ $/\$ $.\/$
16	2, 4, 13, 15	syl3anc 1264	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
17		simpr 462	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
18		hllat 32841	. . . . . . . . . 10
19	2, 18	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20		eqid 2428	. . . . . . . . . . 11
21	20, 8	atbase 32767	. . . . . . . . . 10
22	4, 21	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
23		simp2r 1032	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
24	7, 8, 9, 10	ltrnat 33617	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
25	5, 23, 3, 24	syl3anc 1264	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
26	25	adantr 466	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
27	20, 8	atbase 32767	. . . . . . . . . 10
28	26, 27	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	20, 14, 8	hlatjcl 32844	. . . . . . . . . 10 $/\$ $/\$ $.\/$
30	2, 4, 13, 29	syl3anc 1264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31	20, 7, 14	latjle12 16251	. . . . . . . . 9 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
32	19, 22, 28, 30, 31	syl13anc 1266	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
33	16, 17, 32	mpbi2and 929	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
34		simpl32 1087	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
35	34	necomd 2656	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
36	7, 14, 8	ps-1 32954	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
37	2, 4, 26, 35, 4, 13, 36	syl132anc 1282	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
38	33, 37	mpbid 213	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
39	38	oveq1d 6264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
40		simpl1 1008	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
41		simpl2r 1059	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
42		simpl31 1086	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
43		eqid 2428	. . . . . . 7
44		cdlemg42.r	. . . . . . 7
45	7, 14, 43, 8, 9, 10, 44	trlval2 33641	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
46	40, 41, 42, 45	syl3anc 1264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47		simpl2l 1058	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
48	7, 14, 43, 8, 9, 10, 44	trlval2 33641	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
49	40, 47, 42, 48	syl3anc 1264	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
50	39, 46, 49	3eqtr4rd 2473	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51	50	ex 435	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
52	51	necon3ad 2614	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
53	1, 52	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1872

wne 2599 class class class wbr 4366

cfv 5544 (class class class)co 6249

cbs 15064

cple 15140

cjn 16132

cmee 16133

clat 16234

catm 32741

chlt 32828

clh 33461

cltrn 33578

ctrl 33636

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-mpt2 6254 df-map 7429 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-oposet 32654 df-ol 32656 df-oml 32657 df-covers 32744 df-ats 32745 df-atl 32776 df-cvlat 32800 df-hlat 32829 df-lhyp 33465 df-laut 33466 df-ldil 33581 df-ltrn 33582 df-trl 33637

This theorem is referenced by: cdlemg43 34209

W3C validator