Metamath Proof Explorer

Definition df-cvlat

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)

Ref Expression
Assertion df-cvlat ⊢ CvLat = k ∈ AtLat | ∀ a ∈ Atoms ⁡ k ∀ b ∈ Atoms ⁡ k ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a

Detailed syntax breakdown

Step Hyp Ref Expression
0 clc class CvLat
1 vk setvar k
2 cal class AtLat
3 va setvar a
4 catm class Atoms
5 1 cv setvar k
6 5 4 cfv class Atoms ⁡ k
7 vb setvar b
8 vc setvar c
9 cbs class Base
10 5 9 cfv class Base k
11 3 cv setvar a
12 cple class le
13 5 12 cfv class ≤ k
14 8 cv setvar c
15 11 14 13 wbr wff a ≤ k c
16 15 wn wff ¬ a ≤ k c
17 cjn class join
18 5 17 cfv class join ⁡ k
19 7 cv setvar b
20 14 19 18 co class c join ⁡ k b
21 11 20 13 wbr wff a ≤ k c join ⁡ k b
22 16 21 wa wff ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b
23 14 11 18 co class c join ⁡ k a
24 19 23 13 wbr wff b ≤ k c join ⁡ k a
25 22 24 wi wff ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a
26 25 8 10 wral wff ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a
27 26 7 6 wral wff ∀ b ∈ Atoms ⁡ k ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a
28 27 3 6 wral wff ∀ a ∈ Atoms ⁡ k ∀ b ∈ Atoms ⁡ k ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a
29 28 1 2 crab class k ∈ AtLat | ∀ a ∈ Atoms ⁡ k ∀ b ∈ Atoms ⁡ k ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a
30 0 29 wceq wff CvLat = k ∈ AtLat | ∀ a ∈ Atoms ⁡ k ∀ b ∈ Atoms ⁡ k ∀ c ∈ Base k ¬ a ≤ k c ∧ a ≤ k c join ⁡ k b → b ≤ k c join ⁡ k a