4atexlemc - Mathbox for Norm Megill

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

Theorem 4atexlemc 30258

Description: Lemma for 4atexlem7 30264. (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 30246	. . . 4
4		4thatlem0.j	. . . . 5 $.\/$
5		4thatlem0.a	. . . . 5
6	2, 4, 5	4atexlemqtb 30250	. . . 4 $.\/$
7	2, 4, 5	4atexlempsb 30249	. . . 4 $.\/$
8		eqid 2283	. . . . 5
9		4thatlem0.m	. . . . 5 $./\$
10	8, 9	latmcom 14181	. . . 4 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
11	3, 6, 7, 10	syl3anc 1182	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
12	1, 11	syl5eq 2327	. 2 $.\/$ $./\$ $.\/$
13	2	4atexlemk 30236	. . 3
14	2	4atexlemp 30239	. . 3
15	2	4atexlems 30241	. . 3
16	2	4atexlemq 30240	. . 3
17	2	4atexlemt 30242	. . 3
18		4thatlem0.l	. . . 4
19	2, 18, 4, 5	4atexlempns 30251	. . 3
20		4thatlem0.h	. . . . 5
21		4thatlem0.u	. . . . 5 $.\/$ $./\$
22		4thatlem0.v	. . . . 5 $.\/$ $./\$
23	2, 18, 4, 9, 5, 20, 21, 22	4atexlemntlpq 30257	. . . 4 $.\/$
24	18, 4, 5	atnlej2 29569	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
25	24	necomd 2529	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
26	13, 17, 14, 16, 23, 25	syl131anc 1195	. . 3
27	2	4atexlempnq 30244	. . . 4
28	2	4atexlemnslpq 30245	. . . 4 $.\/$
29	18, 4, 5	4atlem0ae 29783	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30	13, 14, 16, 15, 27, 28, 29	syl132anc 1200	. . 3 $.\/$
31	8, 5	atbase 29479	. . . . 5
32	17, 31	syl 15	. . . 4
33	2, 18, 4, 9, 5, 20, 21	4atexlemu 30253	. . . . 5
34	2, 18, 4, 9, 5, 20, 21, 22	4atexlemv 30254	. . . . 5
35	8, 4, 5	hlatjcl 29556	. . . . 5 $/\$ $/\$ $.\/$
36	13, 33, 34, 35	syl3anc 1182	. . . 4 $.\/$
37	8, 5	atbase 29479	. . . . . 6
38	16, 37	syl 15	. . . . 5
39	8, 4	latjcl 14156	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$
40	3, 7, 38, 39	syl3anc 1182	. . . 4 $.\/$ $.\/$
41	2	4atexlemkc 30247	. . . . 5
42	2, 18, 4, 9, 5, 20, 21, 22	4atexlemunv 30255	. . . . 5
43	2	4atexlemutvt 30243	. . . . 5 $.\/$ $.\/$
44	5, 18, 4	cvlsupr4 29535	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
45	41, 33, 34, 17, 42, 43, 44	syl132anc 1200	. . . 4 $.\/$
46	8, 4, 5	hlatjcl 29556	. . . . . . . . 9 $/\$ $/\$ $.\/$
47	13, 14, 16, 46	syl3anc 1182	. . . . . . . 8 $.\/$
48	2, 20	4atexlemwb 30248	. . . . . . . 8
49	8, 18, 9	latmle1 14182	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
50	3, 47, 48, 49	syl3anc 1182	. . . . . . 7 $.\/$ $./\$ $.\/$
51	21, 50	syl5eqbr 4056	. . . . . 6 $.\/$
52	8, 18, 9	latmle1 14182	. . . . . . . 8 $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$
53	3, 7, 48, 52	syl3anc 1182	. . . . . . 7 $.\/$ $./\$ $.\/$
54	22, 53	syl5eqbr 4056	. . . . . 6 $.\/$
55	8, 5	atbase 29479	. . . . . . . 8
56	33, 55	syl 15	. . . . . . 7
57	8, 5	atbase 29479	. . . . . . . 8
58	34, 57	syl 15	. . . . . . 7
59	8, 18, 4	latjlej12 14173	. . . . . . 7 $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
60	3, 56, 47, 58, 7, 59	syl122anc 1191	. . . . . 6 $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
61	51, 54, 60	mp2and 660	. . . . 5 $.\/$ $.\/$ $.\/$ $.\/$
62	4, 5	hlatjass 29559	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
63	13, 14, 16, 15, 62	syl13anc 1184	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
64	8, 5	atbase 29479	. . . . . . . 8
65	14, 64	syl 15	. . . . . . 7
66	8, 5	atbase 29479	. . . . . . . 8
67	15, 66	syl 15	. . . . . . 7
68	8, 4	latj32 14203	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
69	3, 65, 38, 67, 68	syl13anc 1184	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$
70	8, 4	latjjdi 14209	. . . . . . 7 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
71	3, 65, 38, 67, 70	syl13anc 1184	. . . . . 6 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
72	63, 69, 71	3eqtr3rd 2324	. . . . 5 $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
73	61, 72	breqtrd 4047	. . . 4 $.\/$ $.\/$ $.\/$
74	8, 18, 3, 32, 36, 40, 45, 73	lattrd 14164	. . 3 $.\/$ $.\/$
75	18, 4, 9, 5	2atmat 29750	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$
76	13, 14, 15, 16, 17, 19, 26, 30, 74, 75	syl333anc 1214	. 2 $.\/$ $./\$ $.\/$
77	12, 76	eqeltrd 2357	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 176 $/\$ wa 358 $/\$ w3a 934

wceq 1623

wcel 1684

wne 2446 class class class wbr 4023

cfv 5255 (class class class)co 5858

cbs 13148

cple 13215

cjn 14078

cmee 14079

clat 14151

catm 29453

clc 29455

chlt 29540

clh 30173

This theorem is referenced by: 4atexlemnclw 30259 4atexlemex2 30260 4atexlemcnd 30261

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1635 ax-8 1643 ax-13 1686 ax-14 1688 ax-6 1703 ax-7 1708 ax-11 1715 ax-12 1866 ax-ext 2264 ax-rep 4131 ax-sep 4141 ax-nul 4149 ax-pow 4188 ax-pr 4214 ax-un 4512

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1630 df-eu 2147 df-mo 2148 df-clab 2270 df-cleq 2276 df-clel 2279 df-nfc 2408 df-ne 2448 df-nel 2449 df-ral 2548 df-rex 2549 df-reu 2550 df-rab 2552 df-v 2790 df-sbc 2992 df-csb 3082 df-dif 3155 df-un 3157 df-in 3159 df-ss 3166 df-nul 3456 df-if 3566 df-pw 3627 df-sn 3646 df-pr 3647 df-op 3649 df-uni 3828 df-iun 3907 df-br 4024 df-opab 4078 df-mpt 4079 df-id 4309 df-xp 4695 df-rel 4696 df-cnv 4697 df-co 4698 df-dm 4699 df-rn 4700 df-res 4701 df-ima 4702 df-iota 5219 df-fun 5257 df-fn 5258 df-f 5259 df-f1 5260 df-fo 5261 df-f1o 5262 df-fv 5263 df-ov 5861 df-oprab 5862 df-mpt2 5863 df-1st 6122 df-2nd 6123 df-undef 6298 df-riota 6304 df-poset 14080 df-plt 14092 df-lub 14108 df-glb 14109 df-join 14110 df-meet 14111 df-p0 14145 df-p1 14146 df-lat 14152 df-clat 14214 df-oposet 29366 df-ol 29368 df-oml 29369 df-covers 29456 df-ats 29457 df-atl 29488 df-cvlat 29512 df-hlat 29541 df-llines 29687 df-lplanes 29688 df-lhyp 30177

W3C validator