paddasslem12 - Mathbox for Norm Megill

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

Theorem paddasslem12 32848

Description: Lemma for paddass 32855. The case when

. (Contributed by NM, 11-Jan-2012.)

**Hypotheses**
Ref	Expression
paddasslem.l
paddasslem.j	$.\/$
paddasslem.a
paddasslem.p

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

**Proof of Theorem paddasslem12**
Step	Hyp	Ref	Expression
1		simpl1l 1048	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simpl21 1075	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simpl22 1076	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		paddasslem.a	. . . . . 6
5		paddasslem.p	. . . . . 6
6	4, 5	paddssat 32831	. . . . 5 $/\$ $/\$
7	1, 2, 3, 6	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
8		simpl23 1077	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
9	1, 7, 8	3jca 1177	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$
10	4, 5	sspadd2 32833	. . . 4 $/\$ $/\$
11	1, 3, 2, 10	syl3anc 1230	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
12	4, 5	paddss1 32834	. . 3 $/\$ $/\$
13	9, 11, 12	sylc 59	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
14		hllat 32381	. . . 4
15	1, 14	syl 17	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
16		simprll 764	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
17		simprlr 765	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		simpl3l 1052	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19		eqid 2402	. . . 4
20		paddasslem.l	. . . 4
21	19, 4	atbase 32307	. . . . 5
22	18, 21	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
23	3, 16	sseldd 3443	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
24	19, 4	atbase 32307	. . . . . 6
25	23, 24	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
26		simpl3r 1053	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
27	19, 4	atbase 32307	. . . . . 6
28	26, 27	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
29		paddasslem.j	. . . . . 6 $.\/$
30	19, 29	latjcl 16005	. . . . 5 $/\$ $/\$ $.\/$
31	15, 25, 28, 30	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
32	8, 17	sseldd 3443	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
33	19, 4	atbase 32307	. . . . . 6
34	32, 33	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
35	19, 29	latjcl 16005	. . . . 5 $/\$ $/\$ $.\/$
36	15, 25, 34, 35	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
37		simpl1r 1049	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
38		simprrl 766	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
39		oveq1 6285	. . . . . . 7 $.\/$ $.\/$
40	39	breq2d 4407	. . . . . 6 $.\/$ $.\/$
41	40	biimpa 482	. . . . 5 $/\$ $.\/$ $.\/$
42	37, 38, 41	syl2anc 659	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
43	19, 20, 29	latlej1 16014	. . . . . 6 $/\$ $/\$ $.\/$
44	15, 25, 34, 43	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
45		simprrr 767	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
46	19, 20, 29	latjle12 16016	. . . . . 6 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
47	15, 25, 28, 36, 46	syl13anc 1232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
48	44, 45, 47	mpbi2and 922	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
49	19, 20, 15, 22, 31, 36, 42, 48	lattrd 16012	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
50	20, 29, 4, 5	elpaddri 32819	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51	15, 3, 8, 16, 17, 18, 49, 50	syl322anc 1258	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
52	13, 51	sseldd 3443	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wss 3414 class class class wbr 4395

cfv 5569 (class class class)co 6278

cbs 14841

cple 14916

cjn 15897

clat 15999

catm 32281

chlt 32368

cpadd 32812

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2759 df-rex 2760 df-reu 2761 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-mpt2 6283 df-1st 6784 df-2nd 6785 df-poset 15899 df-lub 15928 df-glb 15929 df-join 15930 df-meet 15931 df-lat 16000 df-ats 32285 df-atl 32316 df-cvlat 32340 df-hlat 32369 df-padd 32813

This theorem is referenced by: paddasslem14 32850

W3C validator