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 35900
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 35843 . 2 class CvLat
2 va . . . . . . . . . . 11 setvar 𝑎
32cv 1506 . . . . . . . . . 10 class 𝑎
4 vc . . . . . . . . . . 11 setvar 𝑐
54cv 1506 . . . . . . . . . 10 class 𝑐
6 vk . . . . . . . . . . . 12 setvar 𝑘
76cv 1506 . . . . . . . . . . 11 class 𝑘
8 cple 16428 . . . . . . . . . . 11 class le
97, 8cfv 6188 . . . . . . . . . 10 class (le‘𝑘)
103, 5, 9wbr 4929 . . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
1110wn 3 . . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12 vb . . . . . . . . . . 11 setvar 𝑏
1312cv 1506 . . . . . . . . . 10 class 𝑏
14 cjn 17412 . . . . . . . . . . 11 class join
157, 14cfv 6188 . . . . . . . . . 10 class (join‘𝑘)
165, 13, 15co 6976 . . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
173, 16, 9wbr 4929 . . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
1811, 17wa 387 . . . . . . 7 wff 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
195, 3, 15co 6976 . . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
2013, 19, 9wbr 4929 . . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
2118, 20wi 4 . . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22 cbs 16339 . . . . . . 7 class Base
237, 22cfv 6188 . . . . . 6 class (Base‘𝑘)
2421, 4, 23wral 3089 . . . . 5 wff 𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25 catm 35841 . . . . . 6 class Atoms
267, 25cfv 6188 . . . . 5 class (Atoms‘𝑘)
2724, 12, 26wral 3089 . . . 4 wff 𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
2827, 2, 26wral 3089 . . 3 wff 𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29 cal 35842 . . 3 class AtLat
3028, 6, 29crab 3093 . 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
311, 30wceq 1507 1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
Colors of variables: wff setvar class
This definition is referenced by:  iscvlat  35901
  Copyright terms: Public domain W3C validator