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 34927
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 34870 . 2 class CvLat
2 va . . . . . . . . . . 11 setvar 𝑎
32cv 1522 . . . . . . . . . 10 class 𝑎
4 vc . . . . . . . . . . 11 setvar 𝑐
54cv 1522 . . . . . . . . . 10 class 𝑐
6 vk . . . . . . . . . . . 12 setvar 𝑘
76cv 1522 . . . . . . . . . . 11 class 𝑘
8 cple 15995 . . . . . . . . . . 11 class le
97, 8cfv 5926 . . . . . . . . . 10 class (le‘𝑘)
103, 5, 9wbr 4685 . . . . . . . . 9 wff 𝑎(le‘𝑘)𝑐
1110wn 3 . . . . . . . 8 wff ¬ 𝑎(le‘𝑘)𝑐
12 vb . . . . . . . . . . 11 setvar 𝑏
1312cv 1522 . . . . . . . . . 10 class 𝑏
14 cjn 16991 . . . . . . . . . . 11 class join
157, 14cfv 5926 . . . . . . . . . 10 class (join‘𝑘)
165, 13, 15co 6690 . . . . . . . . 9 class (𝑐(join‘𝑘)𝑏)
173, 16, 9wbr 4685 . . . . . . . 8 wff 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)
1811, 17wa 383 . . . . . . 7 wff 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏))
195, 3, 15co 6690 . . . . . . . 8 class (𝑐(join‘𝑘)𝑎)
2013, 19, 9wbr 4685 . . . . . . 7 wff 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎)
2118, 20wi 4 . . . . . 6 wff ((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
22 cbs 15904 . . . . . . 7 class Base
237, 22cfv 5926 . . . . . 6 class (Base‘𝑘)
2421, 4, 23wral 2941 . . . . 5 wff 𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
25 catm 34868 . . . . . 6 class Atoms
267, 25cfv 5926 . . . . 5 class (Atoms‘𝑘)
2724, 12, 26wral 2941 . . . 4 wff 𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
2827, 2, 26wral 2941 . . 3 wff 𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))
29 cal 34869 . . 3 class AtLat
3028, 6, 29crab 2945 . 2 class {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
311, 30wceq 1523 1 wff CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))}
Colors of variables: wff setvar class
This definition is referenced by:  iscvlat  34928
  Copyright terms: Public domain W3C validator