Definition df-cvlat 39786

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 39729	. 2 class CvLat
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1541	. . . . . . . . . 10 class 𝑎
4		vc	. . . . . . . . . . 11 setvar 𝑐
5	4	cv 1541	. . . . . . . . . 10 class 𝑐
6		vk	. . . . . . . . . . . 12 setvar 𝑘
7	6	cv 1541	. . . . . . . . . . 11 class 𝑘
8		cple 17222	. . . . . . . . . . 11 class le
9	7, 8	cfv 6494	. . . . . . . . . 10 class (le‘𝑘)
10	3, 5, 9	wbr 5086	. . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
11	10	wn 3	. . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12		vb	. . . . . . . . . . 11 setvar 𝑏
13	12	cv 1541	. . . . . . . . . 10 class 𝑏
14		cjn 18272	. . . . . . . . . . 11 class join
15	7, 14	cfv 6494	. . . . . . . . . 10 class (join‘𝑘)
16	5, 13, 15	co 7362	. . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
17	3, 16, 9	wbr 5086	. . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
18	11, 17	wa 395	. . . . . . 7 wff (¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
19	5, 3, 15	co 7362	. . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
20	13, 19, 9	wbr 5086	. . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
21	18, 20	wi 4	. . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22		cbs 17174	. . . . . . 7 class Base
23	7, 22	cfv 6494	. . . . . 6 class (Base‘𝑘)
24	21, 4, 23	wral 3052	. . . . 5 wff ∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25		catm 39727	. . . . . 6 class Atoms
26	7, 25	cfv 6494	. . . . 5 class (Atoms‘𝑘)
27	24, 12, 26	wral 3052	. . . 4 wff ∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
28	27, 2, 26	wral 3052	. . 3 wff ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29		cal 39728	. . 3 class AtLat
30	28, 6, 29	crab 3390	. 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
31	1, 30	wceq 1542	1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}

This definition is referenced by:  iscvlat  39787