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 36611
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 36554 . 2 class CvLat
2 va . . . . . . . . . . 11 setvar 𝑎
32cv 1537 . . . . . . . . . 10 class 𝑎
4 vc . . . . . . . . . . 11 setvar 𝑐
54cv 1537 . . . . . . . . . 10 class 𝑐
6 vk . . . . . . . . . . . 12 setvar 𝑘
76cv 1537 . . . . . . . . . . 11 class 𝑘
8 cple 16567 . . . . . . . . . . 11 class le
97, 8cfv 6328 . . . . . . . . . 10 class (le‘𝑘)
103, 5, 9wbr 5033 . . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
1110wn 3 . . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12 vb . . . . . . . . . . 11 setvar 𝑏
1312cv 1537 . . . . . . . . . 10 class 𝑏
14 cjn 17549 . . . . . . . . . . 11 class join
157, 14cfv 6328 . . . . . . . . . 10 class (join‘𝑘)
165, 13, 15co 7139 . . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
173, 16, 9wbr 5033 . . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
1811, 17wa 399 . . . . . . 7 wff 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
195, 3, 15co 7139 . . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
2013, 19, 9wbr 5033 . . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
2118, 20wi 4 . . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22 cbs 16478 . . . . . . 7 class Base
237, 22cfv 6328 . . . . . 6 class (Base‘𝑘)
2421, 4, 23wral 3109 . . . . 5 wff 𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25 catm 36552 . . . . . 6 class Atoms
267, 25cfv 6328 . . . . 5 class (Atoms‘𝑘)
2724, 12, 26wral 3109 . . . 4 wff 𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
2827, 2, 26wral 3109 . . 3 wff 𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29 cal 36553 . . 3 class AtLat
3028, 6, 29crab 3113 . 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
311, 30wceq 1538 1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
Colors of variables: wff setvar class
This definition is referenced by:  iscvlat  36612
  Copyright terms: Public domain W3C validator