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 33847

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 990	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
2	1	oveq2d 6107	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
3	2	oveq1d 6106	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
4		simp1l 1012	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
5		simp1rl 1053	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
6		simp21 1021	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
7		cdlemd4.l	. . . . . . 7
8		cdlemd4.j	. . . . . . 7 $.\/$
9		eqid 2443	. . . . . . 7
10		cdlemd4.a	. . . . . . 7
11		cdlemd4.h	. . . . . . 7
12		cdlemd4.t	. . . . . . 7
13		eqid 2443	. . . . . . 7
14	7, 8, 9, 10, 11, 12, 13	trlval2 33807	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
15	4, 5, 6, 14	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
16		simp1rr 1054	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	7, 8, 9, 10, 11, 12, 13	trlval2 33807	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $.\/$
18	4, 16, 6, 17	syl3anc 1218	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19	3, 15, 18	3eqtr4d 2485	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
20	19	oveq2d 6107	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
21	1	oveq1d 6106	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
22	20, 21	oveq12d 6109	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$ $.\/$
23		simp22 1022	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
24		simp23 1023	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
25	7, 8, 9, 10, 11, 12, 13	cdlemc 33841	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
26	4, 5, 6, 23, 24, 25	syl131anc 1231	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
27		oveq2 6099	. . . . . . 7 $.\/$ $.\/$
28	27	breq2d 4304	. . . . . 6 $.\/$ $.\/$
29	28	notbid 294	. . . . 5 $.\/$ $.\/$
30	29	biimpd 207	. . . 4 $.\/$ $.\/$
31	1, 24, 30	sylc 60	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
32	7, 8, 9, 10, 11, 12, 13	cdlemc 33841	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
33	4, 16, 6, 23, 31, 32	syl131anc 1231	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
34	22, 26, 33	3eqtr4d 2485	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1369

wcel 1756 class class class wbr 4292

cfv 5418 (class class class)co 6091

cple 14245

cjn 15114

cmee 15115

catm 32908

chlt 32995

clh 33628

cltrn 33745

ctrl 33802

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4403 ax-sep 4413 ax-nul 4421 ax-pow 4470 ax-pr 4531 ax-un 6372

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2568 df-ne 2608 df-ral 2720 df-rex 2721 df-reu 2722 df-rab 2724 df-v 2974 df-sbc 3187 df-csb 3289 df-dif 3331 df-un 3333 df-in 3335 df-ss 3342 df-nul 3638 df-if 3792 df-pw 3862 df-sn 3878 df-pr 3880 df-op 3884 df-uni 4092 df-iun 4173 df-iin 4174 df-br 4293 df-opab 4351 df-mpt 4352 df-id 4636 df-xp 4846 df-rel 4847 df-cnv 4848 df-co 4849 df-dm 4850 df-rn 4851 df-res 4852 df-ima 4853 df-iota 5381 df-fun 5420 df-fn 5421 df-f 5422 df-f1 5423 df-fo 5424 df-f1o 5425 df-fv 5426 df-riota 6052 df-ov 6094 df-oprab 6095 df-mpt2 6096 df-1st 6577 df-2nd 6578 df-map 7216 df-poset 15116 df-plt 15128 df-lub 15144 df-glb 15145 df-join 15146 df-meet 15147 df-p0 15209 df-p1 15210 df-lat 15216 df-clat 15278 df-oposet 32821 df-ol 32823 df-oml 32824 df-covers 32911 df-ats 32912 df-atl 32943 df-cvlat 32967 df-hlat 32996 df-llines 33142 df-psubsp 33147 df-pmap 33148 df-padd 33440 df-lhyp 33632 df-laut 33633 df-ldil 33748 df-ltrn 33749 df-trl 33803

This theorem is referenced by: cdlemd7 33848

W3C validator