Definition df-cvlat 39727

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 39670	. 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 17198	. . . . . . . . . . 11 class le
9	7, 8	cfv 6502	. . . . . . . . . 10 class (le‘𝑘)
10	3, 5, 9	wbr 5100	. . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
11	10	wn 3	. . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12		vb	. . . . . . . . . . 11 setvar 𝑏
13	12	cv 1541	. . . . . . . . . 10 class 𝑏
14		cjn 18248	. . . . . . . . . . 11 class join
15	7, 14	cfv 6502	. . . . . . . . . 10 class (join‘𝑘)
16	5, 13, 15	co 7370	. . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
17	3, 16, 9	wbr 5100	. . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
18	11, 17	wa 395	. . . . . . 7 wff (¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
19	5, 3, 15	co 7370	. . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
20	13, 19, 9	wbr 5100	. . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
21	18, 20	wi 4	. . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22		cbs 17150	. . . . . . 7 class Base
23	7, 22	cfv 6502	. . . . . 6 class (Base‘𝑘)
24	21, 4, 23	wral 3052	. . . . 5 wff ∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25		catm 39668	. . . . . 6 class Atoms
26	7, 25	cfv 6502	. . . . 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 39669	. . 3 class AtLat
30	28, 6, 29	crab 3401	. 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  39728