4atexlemc - Mathbox for Norm Megill

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

Theorem 4atexlemc 30940

Description: Lemma for 4atexlem7 30946. (Contributed by NM, 24-Nov-2012.)

**Hypotheses**
Ref	Expression
4thatlem.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
4thatlem0.l
4thatlem0.j	$.\/$
4thatlem0.m	$./\$
4thatlem0.a
4thatlem0.h
4thatlem0.u	$.\/$ $./\$
4thatlem0.v	$.\/$ $./\$
4thatlem0.c	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
4atexlemc

**Proof of Theorem 4atexlemc**
Step	Hyp	Ref	Expression
1		4thatlem0.c	. . 3 $.\/$ $./\$ $.\/$
2		4thatlem.ph	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$
3	2	4atexlemkl 30928	. . . 4
4		4thatlem0.j	. . . . 5 $.\/$
5		4thatlem0.a	. . . . 5
6	2, 4, 5	4atexlemqtb 30932	. . . 4 $.\/$
7	2, 4, 5	4atexlempsb 30931	. . . 4 $.\/$
8		eqid 2438	. . . . 5
9		4thatlem0.m	. . . . 5 $./\$
10	8, 9	latmcom 14509	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
11	3, 6, 7, 10	syl3anc 1185	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
12	1, 11	syl5eq 2482	. 2 $.\/$ $./\$ $.\/$
13	2	4atexlemk 30918	. . 3
14	2	4atexlemp 30921	. . 3
15	2	4atexlems 30923	. . 3
16	2	4atexlemq 30922	. . 3
17	2	4atexlemt 30924	. . 3
18		4thatlem0.l	. . . 4
19	2, 18, 4, 5	4atexlempns 30933	. . 3
20		4thatlem0.h	. . . . 5
21		4thatlem0.u	. . . . 5 $.\/$ $./\$
22		4thatlem0.v	. . . . 5 $.\/$ $./\$
23	2, 18, 4, 9, 5, 20, 21, 22	4atexlemntlpq 30939	. . . 4 $.\/$
24	18, 4, 5	atnlej2 30251	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
25	24	necomd 2689	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
26	13, 17, 14, 16, 23, 25	syl131anc 1198	. . 3
27	2	4atexlempnq 30926	. . . 4
28	2	4atexlemnslpq 30927	. . . 4 $.\/$
29	18, 4, 5	4atlem0ae 30465	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30	13, 14, 16, 15, 27, 28, 29	syl132anc 1203	. . 3 $.\/$
31	8, 5	atbase 30161	. . . . 5
32	17, 31	syl 16	. . . 4
33	2, 18, 4, 9, 5, 20, 21	4atexlemu 30935	. . . . 5
34	2, 18, 4, 9, 5, 20, 21, 22	4atexlemv 30936	. . . . 5
35	8, 4, 5	hlatjcl 30238	. . . . 5 $/\$ $/\$ $.\/$
36	13, 33, 34, 35	syl3anc 1185	. . . 4 $.\/$
37	8, 5	atbase 30161	. . . . . 6
38	16, 37	syl 16	. . . . 5
39	8, 4	latjcl 14484	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$
40	3, 7, 38, 39	syl3anc 1185	. . . 4 $.\/$ $.\/$
41	2	4atexlemkc 30929	. . . . 5
42	2, 18, 4, 9, 5, 20, 21, 22	4atexlemunv 30937	. . . . 5
43	2	4atexlemutvt 30925	. . . . 5 $.\/$ $.\/$
44	5, 18, 4	cvlsupr4 30217	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
45	41, 33, 34, 17, 42, 43, 44	syl132anc 1203	. . . 4 $.\/$
46	8, 4, 5	hlatjcl 30238	. . . . . . . . 9 $/\$ $/\$ $.\/$
47	13, 14, 16, 46	syl3anc 1185	. . . . . . . 8 $.\/$
48	2, 20	4atexlemwb 30930	. . . . . . . 8
49	8, 18, 9	latmle1 14510	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
50	3, 47, 48, 49	syl3anc 1185	. . . . . . 7 $.\/$ $./\$ $.\/$
51	21, 50	syl5eqbr 4248	. . . . . 6 $.\/$
52	8, 18, 9	latmle1 14510	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
53	3, 7, 48, 52	syl3anc 1185	. . . . . . 7 $.\/$ $./\$ $.\/$
54	22, 53	syl5eqbr 4248	. . . . . 6 $.\/$
55	8, 5	atbase 30161	. . . . . . . 8
56	33, 55	syl 16	. . . . . . 7
57	8, 5	atbase 30161	. . . . . . . 8
58	34, 57	syl 16	. . . . . . 7
59	8, 18, 4	latjlej12 14501	. . . . . . 7 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
60	3, 56, 47, 58, 7, 59	syl122anc 1194	. . . . . 6 $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
61	51, 54, 60	mp2and 662	. . . . 5 $.\/$ $.\/$ $.\/$ $.\/$
62	4, 5	hlatjass 30241	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
63	13, 14, 16, 15, 62	syl13anc 1187	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
64	8, 5	atbase 30161	. . . . . . . 8
65	14, 64	syl 16	. . . . . . 7
66	8, 5	atbase 30161	. . . . . . . 8
67	15, 66	syl 16	. . . . . . 7
68	8, 4	latj32 14531	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	3, 65, 38, 67, 68	syl13anc 1187	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
70	8, 4	latjjdi 14537	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	3, 65, 38, 67, 70	syl13anc 1187	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
72	63, 69, 71	3eqtr3rd 2479	. . . . 5 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
73	61, 72	breqtrd 4239	. . . 4 $.\/$ $.\/$ $.\/$
74	8, 18, 3, 32, 36, 40, 45, 73	lattrd 14492	. . 3 $.\/$ $.\/$
75	18, 4, 9, 5	2atmat 30432	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
76	13, 14, 15, 16, 17, 19, 26, 30, 74, 75	syl333anc 1217	. 2 $.\/$ $./\$ $.\/$
77	12, 76	eqeltrd 2512	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 178 $/\$ wa 360 $/\$ w3a 937

wceq 1653

wcel 1726

wne 2601 class class class wbr 4215

cfv 5457 (class class class)co 6084

cbs 13474

cple 13541

cjn 14406

cmee 14407

clat 14479

catm 30135

clc 30137

chlt 30222

clh 30855

This theorem is referenced by: 4atexlemnclw 30941 4atexlemex2 30942 4atexlemcnd 30943

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1556 ax-5 1567 ax-17 1627 ax-9 1667 ax-8 1688 ax-13 1728 ax-14 1730 ax-6 1745 ax-7 1750 ax-11 1762 ax-12 1951 ax-ext 2419 ax-rep 4323 ax-sep 4333 ax-nul 4341 ax-pow 4380 ax-pr 4406 ax-un 4704

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3an 939 df-tru 1329 df-ex 1552 df-nf 1555 df-sb 1660 df-eu 2287 df-mo 2288 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2712 df-rex 2713 df-reu 2714 df-rab 2716 df-v 2960 df-sbc 3164 df-csb 3254 df-dif 3325 df-un 3327 df-in 3329 df-ss 3336 df-nul 3631 df-if 3742 df-pw 3803 df-sn 3822 df-pr 3823 df-op 3825 df-uni 4018 df-iun 4097 df-br 4216 df-opab 4270 df-mpt 4271 df-id 4501 df-xp 4887 df-rel 4888 df-cnv 4889 df-co 4890 df-dm 4891 df-rn 4892 df-res 4893 df-ima 4894 df-iota 5421 df-fun 5459 df-fn 5460 df-f 5461 df-f1 5462 df-fo 5463 df-f1o 5464 df-fv 5465 df-ov 6087 df-oprab 6088 df-mpt2 6089 df-1st 6352 df-2nd 6353 df-undef 6546 df-riota 6552 df-poset 14408 df-plt 14420 df-lub 14436 df-glb 14437 df-join 14438 df-meet 14439 df-p0 14473 df-p1 14474 df-lat 14480 df-clat 14542 df-oposet 30048 df-ol 30050 df-oml 30051 df-covers 30138 df-ats 30139 df-atl 30170 df-cvlat 30194 df-hlat 30223 df-llines 30369 df-lplanes 30370 df-lhyp 30859

W3C validator