df-cvlat - Mathbox for Norm Megill

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

Definition df-cvlat 34609

Description: Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.)

**Assertion**
Ref	Expression
df-cvlat	$/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-cvlat**
Step	Hyp	Ref	Expression
1		clc 34552	. 2
2		va	. . . . . . . . . . 11
3	2	cv 1482	. . . . . . . . . 10
4		vc	. . . . . . . . . . 11
5	4	cv 1482	. . . . . . . . . 10
6		vk	. . . . . . . . . . . 12
7	6	cv 1482	. . . . . . . . . . 11
8		cple 15948	. . . . . . . . . . 11
9	7, 8	cfv 5888	. . . . . . . . . 10
10	3, 5, 9	wbr 4653	. . . . . . . . 9
11	10	wn 3	. . . . . . . 8
12		vb	. . . . . . . . . . 11
13	12	cv 1482	. . . . . . . . . 10
14		cjn 16944	. . . . . . . . . . 11
15	7, 14	cfv 5888	. . . . . . . . . 10
16	5, 13, 15	co 6650	. . . . . . . . 9
17	3, 16, 9	wbr 4653	. . . . . . . 8
18	11, 17	wa 384	. . . . . . 7 $/\$
19	5, 3, 15	co 6650	. . . . . . . 8
20	13, 19, 9	wbr 4653	. . . . . . 7
21	18, 20	wi 4	. . . . . 6 $/\$
22		cbs 15857	. . . . . . 7
23	7, 22	cfv 5888	. . . . . 6
24	21, 4, 23	wral 2912	. . . . 5 $/\$
25		catm 34550	. . . . . 6
26	7, 25	cfv 5888	. . . . 5
27	24, 12, 26	wral 2912	. . . 4 $/\$
28	27, 2, 26	wral 2912	. . 3 $/\$
29		cal 34551	. . 3
30	28, 6, 29	crab 2916	. 2 $/\$
31	1, 30	wceq 1483	1 $/\$

Colors of variables: wff setvar class

This definition is referenced by: iscvlat 34610

W3C validator