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