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 38192
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 38135 . 2 class CvLat
2 va . . . . . . . . . . 11 setvar π‘Ž
32cv 1541 . . . . . . . . . 10 class π‘Ž
4 vc . . . . . . . . . . 11 setvar 𝑐
54cv 1541 . . . . . . . . . 10 class 𝑐
6 vk . . . . . . . . . . . 12 setvar π‘˜
76cv 1541 . . . . . . . . . . 11 class π‘˜
8 cple 17204 . . . . . . . . . . 11 class le
97, 8cfv 6544 . . . . . . . . . 10 class (leβ€˜π‘˜)
103, 5, 9wbr 5149 . . . . . . . . 9 wff π‘Ž(leβ€˜π‘˜)𝑐
1110wn 3 . . . . . . . 8 wff Β¬ π‘Ž(leβ€˜π‘˜)𝑐
12 vb . . . . . . . . . . 11 setvar 𝑏
1312cv 1541 . . . . . . . . . 10 class 𝑏
14 cjn 18264 . . . . . . . . . . 11 class join
157, 14cfv 6544 . . . . . . . . . 10 class (joinβ€˜π‘˜)
165, 13, 15co 7409 . . . . . . . . 9 class (𝑐(joinβ€˜π‘˜)𝑏)
173, 16, 9wbr 5149 . . . . . . . 8 wff π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)
1811, 17wa 397 . . . . . . 7 wff (Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏))
195, 3, 15co 7409 . . . . . . . 8 class (𝑐(joinβ€˜π‘˜)π‘Ž)
2013, 19, 9wbr 5149 . . . . . . 7 wff 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž)
2118, 20wi 4 . . . . . 6 wff ((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))
22 cbs 17144 . . . . . . 7 class Base
237, 22cfv 6544 . . . . . 6 class (Baseβ€˜π‘˜)
2421, 4, 23wral 3062 . . . . 5 wff βˆ€π‘ ∈ (Baseβ€˜π‘˜)((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))
25 catm 38133 . . . . . 6 class Atoms
267, 25cfv 6544 . . . . 5 class (Atomsβ€˜π‘˜)
2724, 12, 26wral 3062 . . . 4 wff βˆ€π‘ ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Baseβ€˜π‘˜)((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))
2827, 2, 26wral 3062 . . 3 wff βˆ€π‘Ž ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Baseβ€˜π‘˜)((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))
29 cal 38134 . . 3 class AtLat
3028, 6, 29crab 3433 . 2 class {π‘˜ ∈ AtLat ∣ βˆ€π‘Ž ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Baseβ€˜π‘˜)((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))}
311, 30wceq 1542 1 wff CvLat = {π‘˜ ∈ AtLat ∣ βˆ€π‘Ž ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Atomsβ€˜π‘˜)βˆ€π‘ ∈ (Baseβ€˜π‘˜)((Β¬ π‘Ž(leβ€˜π‘˜)𝑐 ∧ π‘Ž(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)𝑏)) β†’ 𝑏(leβ€˜π‘˜)(𝑐(joinβ€˜π‘˜)π‘Ž))}
Colors of variables: wff setvar class
This definition is referenced by:  iscvlat  38193
  Copyright terms: Public domain W3C validator