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 33898

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 5696	. . . 4
3	1, 2	eqeltri 2508	. . 3
4		nfv 1673	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
5		cdlemefs32a1.z	. . . . . . . 8 $/\$ $.\/$
6		nfra1 2761	. . . . . . . . 9 $/\$ $.\/$
7		nfcv 2574	. . . . . . . . 9
8	6, 7	nfriota 6056	. . . . . . . 8 $/\$ $.\/$
9	5, 8	nfcxfr 2571	. . . . . . 7
10	9	nfel1 2584	. . . . . 6
11		nfcv 2574	. . . . . . . 8
12		nfcv 2574	. . . . . . . 8
13	9, 11, 12	nfbr 4331	. . . . . . 7
14	13	nfn 1835	. . . . . 6
15	10, 14	nfan 1860	. . . . 5 $/\$
16	15	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
17	5	a1i 11	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
18		eleq1 2498	. . . . . 6
19		breq1 4290	. . . . . . 7
20	19	notbid 294	. . . . . 6
21	18, 20	anbi12d 710	. . . . 5 $/\$ $/\$
22	21	adantl 466	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
23		simpl1 991	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
24		simpl2r 1042	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
25		simprl 755	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
26		simprrl 763	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
27	25, 26	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
28		simpl2l 1041	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
29		simpl3 993	. . . . . 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 33732	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
40	31, 32, 33, 34, 35, 36, 37, 38	cdleme7 33733	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
41	39, 40	jca 532	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
42	23, 24, 27, 28, 29, 30, 41	syl123anc 1235	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $/\$
43	42	ex 434	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$
44		simp1 988	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$
45		simp2rl 1057	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
46		simp2rr 1058	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
47		simp2l 1014	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
48		simp3 990	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
49	1, 31, 32, 33, 34, 35, 36, 37, 38, 5	cdleme25cl 33841	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
50	44, 45, 46, 47, 48, 49	syl122anc 1227	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
51		simp11 1018	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
52		simp12 1019	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
53		simp13 1020	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
54	31, 32, 34, 35	cdlemb2 33525	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	51, 52, 53, 47, 54	syl121anc 1223	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
56	4, 16, 17, 22, 43, 50, 55	riotasv3d 32451	. . 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 33872	. . . . 5 $/\$ $.\/$
62	45, 48, 61	syl2anc 661	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
63	62	eleq1d 2504	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
64	62	breq1d 4297	. . . 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 965

wceq 1369

wnf 1589

wcel 1756

wne 2601

wral 2710

wrex 2711

cvv 2967

csb 3283

cif 3786 class class class wbr 4287

cfv 5413

crio 6046 (class class class)co 6086

cbs 14166

cple 14237

cjn 15106

cmee 15107

catm 32748

chlt 32835

clh 33468

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 2419 ax-rep 4398 ax-sep 4408 ax-nul 4416 ax-pow 4465 ax-pr 4526 ax-un 6367 ax-riotaBAD 32444

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2256 df-mo 2257 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2715 df-rex 2716 df-reu 2717 df-rmo 2718 df-rab 2719 df-v 2969 df-sbc 3182 df-csb 3284 df-dif 3326 df-un 3328 df-in 3330 df-ss 3337 df-nul 3633 df-if 3787 df-pw 3857 df-sn 3873 df-pr 3875 df-op 3879 df-uni 4087 df-iun 4168 df-iin 4169 df-br 4288 df-opab 4346 df-mpt 4347 df-id 4631 df-xp 4841 df-rel 4842 df-cnv 4843 df-co 4844 df-dm 4845 df-rn 4846 df-res 4847 df-ima 4848 df-iota 5376 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-riota 6047 df-ov 6089 df-oprab 6090 df-mpt2 6091 df-1st 6572 df-2nd 6573 df-undef 6784 df-poset 15108 df-plt 15120 df-lub 15136 df-glb 15137 df-join 15138 df-meet 15139 df-p0 15201 df-p1 15202 df-lat 15208 df-clat 15270 df-oposet 32661 df-ol 32663 df-oml 32664 df-covers 32751 df-ats 32752 df-atl 32783 df-cvlat 32807 df-hlat 32836 df-llines 32982 df-lplanes 32983 df-lvols 32984 df-lines 32985 df-psubsp 32987 df-pmap 32988 df-padd 33280 df-lhyp 33472

This theorem is referenced by: cdlemefs32snb 33899 cdleme32sn1awN 33916 cdleme32snaw 33919

W3C validator