cdlemefs32sn1aw - Mathbox for Norm Megill

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

Theorem cdlemefs32sn1aw 35566

Description: Show that

is an atom not under

when

$.\/$

. (Contributed by NM, 24-Mar-2013.)

**Hypotheses**
Ref	Expression
cdlemefs32.b
cdlemefs32.l
cdlemefs32.j	$.\/$
cdlemefs32.m	$./\$
cdlemefs32.a
cdlemefs32.h
cdlemefs32.u	$.\/$ $./\$
cdlemefs32.d	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemefs32.e	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemefs32.i	$/\$ $.\/$
cdlemefs32.n	$.\/$
cdlemefs32a1.y	$.\/$ $./\$ $.\/$ $.\/$ $./\$
cdlemefs32a1.z	$/\$ $.\/$

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

Distinct variable groups:

$.\/$ ,

$./\$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

**Proof of Theorem cdlemefs32sn1aw**
Step	Hyp	Ref	Expression
1		cdlemefs32.b	. . . 4
2		fvex 5882	. . . 4
3	1, 2	eqeltri 2551	. . 3
4		nfv 1683	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
5		cdlemefs32a1.z	. . . . . . . 8 $/\$ $.\/$
6		nfra1 2848	. . . . . . . . 9 $/\$ $.\/$
7		nfcv 2629	. . . . . . . . 9
8	6, 7	nfriota 6265	. . . . . . . 8 $/\$ $.\/$
9	5, 8	nfcxfr 2627	. . . . . . 7
10	9	nfel1 2645	. . . . . 6
11		nfcv 2629	. . . . . . . 8
12		nfcv 2629	. . . . . . . 8
13	9, 11, 12	nfbr 4497	. . . . . . 7
14	13	nfn 1849	. . . . . 6
15	10, 14	nfan 1875	. . . . 5 $/\$
16	15	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	5	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		eleq1 2539	. . . . . 6
19		breq1 4456	. . . . . . 7
20	19	notbid 294	. . . . . 6
21	18, 20	anbi12d 710	. . . . 5 $/\$ $/\$
22	21	adantl 466	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
23		simpl1 999	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simpl2r 1050	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simprl 755	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simprrl 763	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	25, 26	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		simpl2l 1049	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29		simpl3 1001	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30		simprrr 764	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
31		cdlemefs32.l	. . . . . . . 8
32		cdlemefs32.j	. . . . . . . 8 $.\/$
33		cdlemefs32.m	. . . . . . . 8 $./\$
34		cdlemefs32.a	. . . . . . . 8
35		cdlemefs32.h	. . . . . . . 8
36		cdlemefs32.u	. . . . . . . 8 $.\/$ $./\$
37		cdlemefs32.d	. . . . . . . 8 $.\/$ $./\$ $.\/$ $.\/$ $./\$
38		cdlemefs32a1.y	. . . . . . . 8 $.\/$ $./\$ $.\/$ $.\/$ $./\$
39	31, 32, 33, 34, 35, 36, 37, 38	cdleme7ga 35400	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
40	31, 32, 33, 34, 35, 36, 37, 38	cdleme7 35401	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41	39, 40	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
42	23, 24, 27, 28, 29, 30, 41	syl123anc 1245	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
43	42	ex 434	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$
44		simp1 996	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp2rl 1065	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
46		simp2rr 1066	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
47		simp2l 1022	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
48		simp3 998	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
49	1, 31, 32, 33, 34, 35, 36, 37, 38, 5	cdleme25cl 35509	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
50	44, 45, 46, 47, 48, 49	syl122anc 1237	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp11 1026	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
52		simp12 1027	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp13 1028	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	31, 32, 34, 35	cdlemb2 35193	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	51, 52, 53, 47, 54	syl121anc 1233	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	4, 16, 17, 22, 43, 50, 55	riotasv3d 34119	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
57	3, 56	mpan2 671	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		cdlemefs32.e	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
59		cdlemefs32.i	. . . . . 6 $/\$ $.\/$
60		cdlemefs32.n	. . . . . 6 $.\/$
61	58, 59, 60, 38, 5	cdleme31sn1c 35540	. . . . 5 $/\$ $.\/$
62	45, 48, 61	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	62	eleq1d 2536	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
64	62	breq1d 4463	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
65	64	notbid 294	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
66	63, 65	anbi12d 710	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
67	57, 66	mpbird 232	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1379

wnf 1599

wcel 1767

wne 2662

wral 2817

wrex 2818

cvv 3118

csb 3440

cif 3945 class class class wbr 4453

cfv 5594

crio 6255 (class class class)co 6295

cbs 14507

cple 14579

cjn 15448

cmee 15449

catm 34416

chlt 34503

clh 35136

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-riotaBAD 34112

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-op 4040 df-uni 4252 df-iun 4333 df-iin 4334 df-br 4454 df-opab 4512 df-mpt 4513 df-id 4801 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-riota 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-1st 6795 df-2nd 6796 df-undef 7014 df-poset 15450 df-plt 15462 df-lub 15478 df-glb 15479 df-join 15480 df-meet 15481 df-p0 15543 df-p1 15544 df-lat 15550 df-clat 15612 df-oposet 34329 df-ol 34331 df-oml 34332 df-covers 34419 df-ats 34420 df-atl 34451 df-cvlat 34475 df-hlat 34504 df-llines 34650 df-lplanes 34651 df-lvols 34652 df-lines 34653 df-psubsp 34655 df-pmap 34656 df-padd 34948 df-lhyp 35140

This theorem is referenced by: cdlemefs32snb 35567 cdleme32sn1awN 35584 cdleme32snaw 35587

W3C validator