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 33690

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 5891	. . . 4
3	1, 2	eqeltri 2513	. . 3
4		nfv 1754	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
5		cdlemefs32a1.z	. . . . . . . 8 $/\$ $.\/$
6		nfra1 2813	. . . . . . . . 9 $/\$ $.\/$
7		nfcv 2591	. . . . . . . . 9
8	6, 7	nfriota 6276	. . . . . . . 8 $/\$ $.\/$
9	5, 8	nfcxfr 2589	. . . . . . 7
10	9	nfel1 2607	. . . . . 6
11		nfcv 2591	. . . . . . . 8
12		nfcv 2591	. . . . . . . 8
13	9, 11, 12	nfbr 4470	. . . . . . 7
14	13	nfn 1958	. . . . . 6
15	10, 14	nfan 1986	. . . . 5 $/\$
16	15	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	5	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		eleq1 2501	. . . . . 6
19		breq1 4429	. . . . . . 7
20	19	notbid 295	. . . . . 6
21	18, 20	anbi12d 715	. . . . 5 $/\$ $/\$
22	21	adantl 467	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
23		simpl1 1008	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simpl2r 1059	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simprl 762	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simprrl 772	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	25, 26	jca 534	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		simpl2l 1058	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29		simpl3 1010	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
30		simprrr 773	. . . . . 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 33523	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
40	31, 32, 33, 34, 35, 36, 37, 38	cdleme7 33524	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41	39, 40	jca 534	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
42	23, 24, 27, 28, 29, 30, 41	syl123anc 1281	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
43	42	ex 435	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$
44		simp1 1005	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp2rl 1074	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
46		simp2rr 1075	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
47		simp2l 1031	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
48		simp3 1007	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
49	1, 31, 32, 33, 34, 35, 36, 37, 38, 5	cdleme25cl 33633	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
50	44, 45, 46, 47, 48, 49	syl122anc 1273	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp11 1035	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
52		simp12 1036	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp13 1037	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	31, 32, 34, 35	cdlemb2 33315	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	51, 52, 53, 47, 54	syl121anc 1269	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	4, 16, 17, 22, 43, 50, 55	riotasv3d 32241	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
57	3, 56	mpan2 675	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
58		cdlemefs32.e	. . . . . 6 $.\/$ $./\$ $.\/$ $.\/$ $./\$
59		cdlemefs32.i	. . . . . 6 $/\$ $.\/$
60		cdlemefs32.n	. . . . . 6 $.\/$
61	58, 59, 60, 38, 5	cdleme31sn1c 33664	. . . . 5 $/\$ $.\/$
62	45, 48, 61	syl2anc 665	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	62	eleq1d 2498	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
64	62	breq1d 4436	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
65	64	notbid 295	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
66	63, 65	anbi12d 715	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$
67	57, 66	mpbird 235	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wnf 1663

wcel 1870

wne 2625

wral 2782

wrex 2783

cvv 3087

csb 3401

cif 3915 class class class wbr 4426

cfv 5601

crio 6266 (class class class)co 6305

cbs 15084

cple 15159

cjn 16140

cmee 16141

catm 32538

chlt 32625

clh 33258

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597 ax-riotaBAD 32234

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-nel 2628 df-ral 2787 df-rex 2788 df-reu 2789 df-rmo 2790 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-op 4009 df-uni 4223 df-iun 4304 df-iin 4305 df-br 4427 df-opab 4485 df-mpt 4486 df-id 4769 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-mpt2 6310 df-1st 6807 df-2nd 6808 df-undef 7028 df-preset 16124 df-poset 16142 df-plt 16155 df-lub 16171 df-glb 16172 df-join 16173 df-meet 16174 df-p0 16236 df-p1 16237 df-lat 16243 df-clat 16305 df-oposet 32451 df-ol 32453 df-oml 32454 df-covers 32541 df-ats 32542 df-atl 32573 df-cvlat 32597 df-hlat 32626 df-llines 32772 df-lplanes 32773 df-lvols 32774 df-lines 32775 df-psubsp 32777 df-pmap 32778 df-padd 33070 df-lhyp 33262

This theorem is referenced by: cdlemefs32snb 33691 cdleme32sn1awN 33708 cdleme32snaw 33711

W3C validator