cdlemefs32sn1aw - Mathbox for Norm Megill

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

Theorem cdlemefs32sn1aw 34052

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 5889	. . . 4
3	1, 2	eqeltri 2545	. . 3
4		nfv 1769	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
5		cdlemefs32a1.z	. . . . . . . 8 $/\$ $.\/$
6		nfra1 2785	. . . . . . . . 9 $/\$ $.\/$
7		nfcv 2612	. . . . . . . . 9
8	6, 7	nfriota 6279	. . . . . . . 8 $/\$ $.\/$
9	5, 8	nfcxfr 2610	. . . . . . 7
10	9	nfel1 2626	. . . . . 6
11		nfcv 2612	. . . . . . . 8
12		nfcv 2612	. . . . . . . 8
13	9, 11, 12	nfbr 4440	. . . . . . 7
14	13	nfn 2003	. . . . . 6
15	10, 14	nfan 2031	. . . . 5 $/\$
16	15	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	5	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		eleq1 2537	. . . . . 6
19		breq1 4398	. . . . . . 7
20	19	notbid 301	. . . . . 6
21	18, 20	anbi12d 725	. . . . 5 $/\$ $/\$
22	21	adantl 473	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
23		simpl1 1033	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simpl2r 1084	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simprl 772	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simprrl 782	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	25, 26	jca 541	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		simpl2l 1083	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29		simpl3 1035	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30		simprrr 783	. . . . . 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 33885	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
40	31, 32, 33, 34, 35, 36, 37, 38	cdleme7 33886	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41	39, 40	jca 541	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
42	23, 24, 27, 28, 29, 30, 41	syl123anc 1309	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
43	42	ex 441	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$
44		simp1 1030	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp2rl 1099	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
46		simp2rr 1100	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
47		simp2l 1056	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
48		simp3 1032	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
49	1, 31, 32, 33, 34, 35, 36, 37, 38, 5	cdleme25cl 33995	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
50	44, 45, 46, 47, 48, 49	syl122anc 1301	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp11 1060	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
52		simp12 1061	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp13 1062	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	31, 32, 34, 35	cdlemb2 33677	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	51, 52, 53, 47, 54	syl121anc 1297	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	4, 16, 17, 22, 43, 50, 55	riotasv3d 32596	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
57	3, 56	mpan2 685	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		cdlemefs32.e	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
59		cdlemefs32.i	. . . . . 6 $/\$ $.\/$
60		cdlemefs32.n	. . . . . 6 $.\/$
61	58, 59, 60, 38, 5	cdleme31sn1c 34026	. . . . 5 $/\$ $.\/$
62	45, 48, 61	syl2anc 673	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	62	eleq1d 2533	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
64	62	breq1d 4405	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
65	64	notbid 301	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
66	63, 65	anbi12d 725	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
67	57, 66	mpbird 240	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 376 $/\$ w3a 1007

wceq 1452

wnf 1675

wcel 1904

wne 2641

wral 2756

wrex 2757

cvv 3031

csb 3349

cif 3872 class class class wbr 4395

cfv 5589

crio 6269 (class class class)co 6308

cbs 15199

cple 15275

cjn 16267

cmee 16268

catm 32900

chlt 32987

clh 33620

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-rep 4508 ax-sep 4518 ax-nul 4527 ax-pow 4579 ax-pr 4639 ax-un 6602 ax-riotaBAD 32589

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3or 1008 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-nel 2644 df-ral 2761 df-rex 2762 df-reu 2763 df-rmo 2764 df-rab 2765 df-v 3033 df-sbc 3256 df-csb 3350 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-pw 3944 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-iun 4271 df-iin 4272 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-rn 4850 df-res 4851 df-ima 4852 df-iota 5553 df-fun 5591 df-fn 5592 df-f 5593 df-f1 5594 df-fo 5595 df-f1o 5596 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313 df-1st 6812 df-2nd 6813 df-undef 7038 df-preset 16251 df-poset 16269 df-plt 16282 df-lub 16298 df-glb 16299 df-join 16300 df-meet 16301 df-p0 16363 df-p1 16364 df-lat 16370 df-clat 16432 df-oposet 32813 df-ol 32815 df-oml 32816 df-covers 32903 df-ats 32904 df-atl 32935 df-cvlat 32959 df-hlat 32988 df-llines 33134 df-lplanes 33135 df-lvols 33136 df-lines 33137 df-psubsp 33139 df-pmap 33140 df-padd 33432 df-lhyp 33624

This theorem is referenced by: cdlemefs32snb 34053 cdleme32sn1awN 34070 cdleme32snaw 34073

W3C validator