Definition df-cvlat 37378

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 37321	. 2 class CvLat
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1538	. . . . . . . . . 10 class 𝑎
4		vc	. . . . . . . . . . 11 setvar 𝑐
5	4	cv 1538	. . . . . . . . . 10 class 𝑐
6		vk	. . . . . . . . . . . 12 setvar 𝑘
7	6	cv 1538	. . . . . . . . . . 11 class 𝑘
8		cple 17014	. . . . . . . . . . 11 class le
9	7, 8	cfv 6458	. . . . . . . . . 10 class (le‘𝑘)
10	3, 5, 9	wbr 5081	. . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
11	10	wn 3	. . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12		vb	. . . . . . . . . . 11 setvar 𝑏
13	12	cv 1538	. . . . . . . . . 10 class 𝑏
14		cjn 18074	. . . . . . . . . . 11 class join
15	7, 14	cfv 6458	. . . . . . . . . 10 class (join‘𝑘)
16	5, 13, 15	co 7307	. . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
17	3, 16, 9	wbr 5081	. . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
18	11, 17	wa 397	. . . . . . 7 wff (¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
19	5, 3, 15	co 7307	. . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
20	13, 19, 9	wbr 5081	. . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
21	18, 20	wi 4	. . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22		cbs 16957	. . . . . . 7 class Base
23	7, 22	cfv 6458	. . . . . 6 class (Base‘𝑘)
24	21, 4, 23	wral 3062	. . . . 5 wff ∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25		catm 37319	. . . . . 6 class Atoms
26	7, 25	cfv 6458	. . . . 5 class (Atoms‘𝑘)
27	24, 12, 26	wral 3062	. . . 4 wff ∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
28	27, 2, 26	wral 3062	. . 3 wff ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29		cal 37320	. . 3 class AtLat
30	28, 6, 29	crab 3284	. 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
31	1, 30	wceq 1539	1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}

This definition is referenced by:  iscvlat  37379