3atlem1 - Mathbox for Norm Megill

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

Theorem 3atlem1 32964

Description: Lemma for 3at 32971. (Contributed by NM, 22-Jun-2012.)

**Hypotheses**
Ref	Expression
3at.l
3at.j	$.\/$
3at.a

**Assertion**
Ref	Expression
3atlem1	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

**Proof of Theorem 3atlem1**
Step	Hyp	Ref	Expression
1		simp11 1035	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
2		simp131 1140	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
3		simp132 1141	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
4		simp133 1142	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
5		3at.j	. . . . . 6 $.\/$
6		3at.a	. . . . . 6
7	5, 6	hlatjass 32851	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
8	1, 2, 3, 4, 7	syl13anc 1266	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
9		simp121 1137	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
10		simp122 1138	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
11		simp123 1139	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
12	5, 6	hlatjass 32851	. . . . . . . . . 10 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
13	1, 9, 10, 11, 12	syl13anc 1266	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
14		simp3 1007	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
15	13, 14	eqbrtrrd 4443	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
16		hllat 32845	. . . . . . . . . 10
17	1, 16	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
18		eqid 2422	. . . . . . . . . . 11
19	18, 6	atbase 32771	. . . . . . . . . 10
20	9, 19	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
21	18, 5, 6	hlatjcl 32848	. . . . . . . . . 10 $/\$ $/\$ $.\/$
22	1, 10, 11, 21	syl3anc 1264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
23	18, 5, 6	hlatjcl 32848	. . . . . . . . . . 11 $/\$ $/\$ $.\/$
24	1, 2, 3, 23	syl3anc 1264	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
25	18, 6	atbase 32771	. . . . . . . . . . 11
26	4, 25	syl 17	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
27	18, 5	latjcl 16282	. . . . . . . . . 10 $/\$ $.\/$ $/\$ $.\/$ $.\/$
28	17, 24, 26, 27	syl3anc 1264	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
29		3at.l	. . . . . . . . . 10
30	18, 29, 5	latjle12 16293	. . . . . . . . 9 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
31	17, 20, 22, 28, 30	syl13anc 1266	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
32	15, 31	mpbird 235	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
33	32	simpld 460	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
34	33, 8	breqtrd 4445	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
35	18, 5, 6	hlatjcl 32848	. . . . . . 7 $/\$ $/\$ $.\/$
36	1, 3, 4, 35	syl3anc 1264	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
37		simp22 1039	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
38	18, 29, 5, 6	hlexchb2 32866	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
39	1, 9, 2, 36, 37, 38	syl131anc 1277	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
40	34, 39	mpbid 213	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
41	5, 6	hlatj12 32852	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
42	1, 9, 3, 4, 41	syl13anc 1266	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
43	8, 40, 42	3eqtr2d 2469	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
44	5, 6	hlatj12 32852	. . . . . . . 8 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
45	1, 9, 10, 11, 44	syl13anc 1266	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
46	15, 45, 43	3brtr3d 4450	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
47	18, 6	atbase 32771	. . . . . . . 8
48	10, 47	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
49	18, 5, 6	hlatjcl 32848	. . . . . . . 8 $/\$ $/\$ $.\/$
50	1, 9, 11, 49	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
51	18, 6	atbase 32771	. . . . . . . . 9
52	3, 51	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
53	18, 5, 6	hlatjcl 32848	. . . . . . . . 9 $/\$ $/\$ $.\/$
54	1, 9, 4, 53	syl3anc 1264	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
55	18, 5	latjcl 16282	. . . . . . . 8 $/\$ $/\$ $.\/$ $.\/$ $.\/$
56	17, 52, 54, 55	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
57	18, 29, 5	latjle12 16293	. . . . . . 7 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
58	17, 48, 50, 56, 57	syl13anc 1266	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
59	46, 58	mpbird 235	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
60	59	simpld 460	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
61		simp23 1040	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
62	18, 29, 5, 6	hlexchb2 32866	. . . . 5 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
63	1, 10, 3, 54, 61, 62	syl131anc 1277	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
64	60, 63	mpbid 213	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
65	18, 5	latj13 16329	. . . 4 $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
66	17, 48, 20, 26, 65	syl13anc 1266	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
67	43, 64, 66	3eqtr2d 2469	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
68	18, 5, 6	hlatjcl 32848	. . . . . . . 8 $/\$ $/\$ $.\/$
69	1, 9, 10, 68	syl3anc 1264	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
70	18, 6	atbase 32771	. . . . . . . 8
71	11, 70	syl 17	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
72	18, 29, 5	latjle12 16293	. . . . . . 7 $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
73	17, 69, 71, 28, 72	syl13anc 1266	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
74	14, 73	mpbird 235	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
75	74	simprd 464	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
76	75, 67	breqtrd 4445	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
77		simp21 1038	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
78	18, 29, 5, 6	hlexchb2 32866	. . . 4 $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
79	1, 11, 4, 69, 77, 78	syl131anc 1277	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
80	76, 79	mpbid 213	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
81	18, 5	latjcom 16290	. . 3 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
82	17, 71, 69, 81	syl3anc 1264	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
83	67, 80, 82	3eqtr2rd 2470	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1437

wcel 1868 class class class wbr 4420

cfv 5597 (class class class)co 6301

cbs 15106

cple 15182

cjn 16174

clat 16276

catm 32745

chlt 32832

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1748 ax-6 1794 ax-7 1839 ax-8 1870 ax-9 1872 ax-10 1887 ax-11 1892 ax-12 1905 ax-13 2053 ax-ext 2400 ax-rep 4533 ax-sep 4543 ax-nul 4551 ax-pow 4598 ax-pr 4656 ax-un 6593

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1787 df-eu 2269 df-mo 2270 df-clab 2408 df-cleq 2414 df-clel 2417 df-nfc 2572 df-ne 2620 df-ral 2780 df-rex 2781 df-reu 2782 df-rab 2784 df-v 3083 df-sbc 3300 df-csb 3396 df-dif 3439 df-un 3441 df-in 3443 df-ss 3450 df-nul 3762 df-if 3910 df-pw 3981 df-sn 3997 df-pr 3999 df-op 4003 df-uni 4217 df-iun 4298 df-br 4421 df-opab 4480 df-mpt 4481 df-id 4764 df-xp 4855 df-rel 4856 df-cnv 4857 df-co 4858 df-dm 4859 df-rn 4860 df-res 4861 df-ima 4862 df-iota 5561 df-fun 5599 df-fn 5600 df-f 5601 df-f1 5602 df-fo 5603 df-f1o 5604 df-fv 5605 df-riota 6263 df-ov 6304 df-oprab 6305 df-preset 16158 df-poset 16176 df-lub 16205 df-glb 16206 df-join 16207 df-meet 16208 df-lat 16277 df-ats 32749 df-atl 32780 df-cvlat 32804 df-hlat 32833

This theorem is referenced by: 3atlem3 32966

W3C validator