Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cvlat Structured version   Visualization version   GIF version

Definition df-cvlat 39303
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
StepHypRef Expression
1 clc 39246 . 2 class CvLat
2 va . . . . . . . . . . 11 setvar 𝑎
32cv 1535 . . . . . . . . . 10 class 𝑎
4 vc . . . . . . . . . . 11 setvar 𝑐
54cv 1535 . . . . . . . . . 10 class 𝑐
6 vk . . . . . . . . . . . 12 setvar 𝑘
76cv 1535 . . . . . . . . . . 11 class 𝑘
8 cple 17304 . . . . . . . . . . 11 class le
97, 8cfv 6562 . . . . . . . . . 10 class (le‘𝑘)
103, 5, 9wbr 5147 . . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
1110wn 3 . . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12 vb . . . . . . . . . . 11 setvar 𝑏
1312cv 1535 . . . . . . . . . 10 class 𝑏
14 cjn 18368 . . . . . . . . . . 11 class join
157, 14cfv 6562 . . . . . . . . . 10 class (join‘𝑘)
165, 13, 15co 7430 . . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
173, 16, 9wbr 5147 . . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
1811, 17wa 395 . . . . . . 7 wff 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
195, 3, 15co 7430 . . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
2013, 19, 9wbr 5147 . . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
2118, 20wi 4 . . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22 cbs 17244 . . . . . . 7 class Base
237, 22cfv 6562 . . . . . 6 class (Base‘𝑘)
2421, 4, 23wral 3058 . . . . 5 wff 𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25 catm 39244 . . . . . 6 class Atoms
267, 25cfv 6562 . . . . 5 class (Atoms‘𝑘)
2724, 12, 26wral 3058 . . . 4 wff 𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
2827, 2, 26wral 3058 . . 3 wff 𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29 cal 39245 . . 3 class AtLat
3028, 6, 29crab 3432 . 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
311, 30wceq 1536 1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
Colors of variables: wff setvar class
This definition is referenced by:  iscvlat  39304
  Copyright terms: Public domain W3C validator