Definition df-cvlat 39322

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 39265	. 2 class CvLat
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1539	. . . . . . . . . 10 class 𝑎
4		vc	. . . . . . . . . . 11 setvar 𝑐
5	4	cv 1539	. . . . . . . . . 10 class 𝑐
6		vk	. . . . . . . . . . . 12 setvar 𝑘
7	6	cv 1539	. . . . . . . . . . 11 class 𝑘
8		cple 17234	. . . . . . . . . . 11 class le
9	7, 8	cfv 6514	. . . . . . . . . 10 class (le‘𝑘)
10	3, 5, 9	wbr 5110	. . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
11	10	wn 3	. . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12		vb	. . . . . . . . . . 11 setvar 𝑏
13	12	cv 1539	. . . . . . . . . 10 class 𝑏
14		cjn 18279	. . . . . . . . . . 11 class join
15	7, 14	cfv 6514	. . . . . . . . . 10 class (join‘𝑘)
16	5, 13, 15	co 7390	. . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
17	3, 16, 9	wbr 5110	. . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
18	11, 17	wa 395	. . . . . . 7 wff (¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
19	5, 3, 15	co 7390	. . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
20	13, 19, 9	wbr 5110	. . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
21	18, 20	wi 4	. . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22		cbs 17186	. . . . . . 7 class Base
23	7, 22	cfv 6514	. . . . . 6 class (Base‘𝑘)
24	21, 4, 23	wral 3045	. . . . 5 wff ∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25		catm 39263	. . . . . 6 class Atoms
26	7, 25	cfv 6514	. . . . 5 class (Atoms‘𝑘)
27	24, 12, 26	wral 3045	. . . 4 wff ∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
28	27, 2, 26	wral 3045	. . 3 wff ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29		cal 39264	. . 3 class AtLat
30	28, 6, 29	crab 3408	. 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
31	1, 30	wceq 1540	1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}

This definition is referenced by:  iscvlat  39323