Definition df-cvlat 40124

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	⊢ CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}

Distinct variable group:   𝑘,𝑐,𝑎,𝑏

Detailed syntax breakdown of Definition df-cvlat

Step	Hyp	Ref	Expression
1		clc 40067	. 2 class CvLat
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1569	. . . . . . . . . 10 class 𝑎
4		vc	. . . . . . . . . . 11 setvar 𝑐
5	4	cv 1569	. . . . . . . . . 10 class 𝑐
6		vk	. . . . . . . . . . . 12 setvar 𝑘
7	6	cv 1569	. . . . . . . . . . 11 class 𝑘
8		cple 17321	. . . . . . . . . . 11 class le
9	7, 8	cfv 6536	. . . . . . . . . 10 class (le‘𝑘)
10	3, 5, 9	wbr 5109	. . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
11	10	wn 3	. . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12		vb	. . . . . . . . . . 11 setvar 𝑏
13	12	cv 1569	. . . . . . . . . 10 class 𝑏
14		cjn 18371	. . . . . . . . . . 11 class join
15	7, 14	cfv 6536	. . . . . . . . . 10 class (join‘𝑘)
16	5, 13, 15	co 7410	. . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
17	3, 16, 9	wbr 5109	. . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
18	11, 17	wa 400	. . . . . . 7 wff (¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
19	5, 3, 15	co 7410	. . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
20	13, 19, 9	wbr 5109	. . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
21	18, 20	wi 4	. . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22		cbs 17273	. . . . . . 7 class Base
23	7, 22	cfv 6536	. . . . . 6 class (Base‘𝑘)
24	21, 4, 23	wral 3079	. . . . 5 wff ∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25		catm 40065	. . . . . 6 class Atoms
26	7, 25	cfv 6536	. . . . 5 class (Atoms‘𝑘)
27	24, 12, 26	wral 3079	. . . 4 wff ∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
28	27, 2, 26	wral 3079	. . 3 wff ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29		cal 40066	. . 3 class AtLat
30	28, 6, 29	crab 3416	. 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
31	1, 30	wceq 1570	1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}

This definition is used by:  iscvlat  40125