cdlemd6 - Mathbox for Norm Megill

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

Theorem cdlemd6 33202

Description: Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.)

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

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

**Proof of Theorem cdlemd6**
Step	Hyp	Ref	Expression
1		simp3 999	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2	1	oveq2d 6250	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
3	2	oveq1d 6249	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
4		simp1l 1021	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		simp1rl 1062	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
6		simp21 1030	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
7		cdlemd4.l	. . . . . . 7
8		cdlemd4.j	. . . . . . 7 $.\/$
9		eqid 2402	. . . . . . 7
10		cdlemd4.a	. . . . . . 7
11		cdlemd4.h	. . . . . . 7
12		cdlemd4.t	. . . . . . 7
13		eqid 2402	. . . . . . 7
14	7, 8, 9, 10, 11, 12, 13	trlval2 33162	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
15	4, 5, 6, 14	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
16		simp1rr 1063	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	7, 8, 9, 10, 11, 12, 13	trlval2 33162	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
18	4, 16, 6, 17	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19	3, 15, 18	3eqtr4d 2453	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
20	19	oveq2d 6250	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
21	1	oveq1d 6249	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	20, 21	oveq12d 6252	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
23		simp22 1031	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
24		simp23 1032	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
25	7, 8, 9, 10, 11, 12, 13	cdlemc 33196	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
26	4, 5, 6, 23, 24, 25	syl131anc 1243	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
27		oveq2 6242	. . . . . . 7 $.\/$ $.\/$
28	27	breq2d 4406	. . . . . 6 $.\/$ $.\/$
29	28	notbid 292	. . . . 5 $.\/$ $.\/$
30	29	biimpd 207	. . . 4 $.\/$ $.\/$
31	1, 24, 30	sylc 59	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32	7, 8, 9, 10, 11, 12, 13	cdlemc 33196	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
33	4, 16, 6, 23, 31, 32	syl131anc 1243	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
34	22, 26, 33	3eqtr4d 2453	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842 class class class wbr 4394

cfv 5525 (class class class)co 6234

cple 14808

cjn 15789

cmee 15790

catm 32262

chlt 32349

clh 32982

cltrn 33099

ctrl 33157

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 4506 ax-sep 4516 ax-nul 4524 ax-pow 4571 ax-pr 4629 ax-un 6530

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 2758 df-rex 2759 df-reu 2760 df-rab 2762 df-v 3060 df-sbc 3277 df-csb 3373 df-dif 3416 df-un 3418 df-in 3420 df-ss 3427 df-nul 3738 df-if 3885 df-pw 3956 df-sn 3972 df-pr 3974 df-op 3978 df-uni 4191 df-iun 4272 df-iin 4273 df-br 4395 df-opab 4453 df-mpt 4454 df-id 4737 df-xp 4948 df-rel 4949 df-cnv 4950 df-co 4951 df-dm 4952 df-rn 4953 df-res 4954 df-ima 4955 df-iota 5489 df-fun 5527 df-fn 5528 df-f 5529 df-f1 5530 df-fo 5531 df-f1o 5532 df-fv 5533 df-riota 6196 df-ov 6237 df-oprab 6238 df-mpt2 6239 df-1st 6738 df-2nd 6739 df-map 7379 df-preset 15773 df-poset 15791 df-plt 15804 df-lub 15820 df-glb 15821 df-join 15822 df-meet 15823 df-p0 15885 df-p1 15886 df-lat 15892 df-clat 15954 df-oposet 32175 df-ol 32177 df-oml 32178 df-covers 32265 df-ats 32266 df-atl 32297 df-cvlat 32321 df-hlat 32350 df-llines 32496 df-psubsp 32501 df-pmap 32502 df-padd 32794 df-lhyp 32986 df-laut 32987 df-ldil 33102 df-ltrn 33103 df-trl 33158

This theorem is referenced by: cdlemd7 33203

W3C validator