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 = { 𝑘 ∈ AtLat ∣ ∀ 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 clc ⊢ CvLat
1 vk ⊢ 𝑘
2 cal ⊢ AtLat
3 va ⊢ 𝑎
4 catm ⊢ Atoms
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( Atoms ‘ 𝑘 )
7 vb ⊢ 𝑏
8 vc ⊢ 𝑐
9 cbs ⊢ Base
10 5 9 cfv ⊢ ( Base ‘ 𝑘 )
11 3 cv ⊢ 𝑎
12 cple ⊢ le
13 5 12 cfv ⊢ ( le ‘ 𝑘 )
14 8 cv ⊢ 𝑐
15 11 14 13 wbr ⊢ 𝑎 ( le ‘ 𝑘 ) 𝑐
16 15 wn ⊢ ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐
17 cjn ⊢ join
18 5 17 cfv ⊢ ( join ‘ 𝑘 )
19 7 cv ⊢ 𝑏
20 14 19 18 co ⊢ ( 𝑐 ( join ‘ 𝑘 ) 𝑏 )
21 11 20 13 wbr ⊢ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 )
22 16 21 wa ⊢ ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) )
23 14 11 18 co ⊢ ( 𝑐 ( join ‘ 𝑘 ) 𝑎 )
24 19 23 13 wbr ⊢ 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 )
25 22 24 wi ⊢ ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) )
26 25 8 10 wral ⊢ ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) )
27 26 7 6 wral ⊢ ∀ 𝑏 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) )
28 27 3 6 wral ⊢ ∀ 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) )
29 28 1 2 crab ⊢ { 𝑘 ∈ AtLat ∣ ∀ 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) ) }
30 0 29 wceq ⊢ CvLat = { 𝑘 ∈ AtLat ∣ ∀ 𝑎 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑏 ∈ ( Atoms ‘ 𝑘 ) ∀ 𝑐 ∈ ( Base ‘ 𝑘 ) ( ( ¬ 𝑎 ( le ‘ 𝑘 ) 𝑐 ∧ 𝑎 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑏 ) ) → 𝑏 ( le ‘ 𝑘 ) ( 𝑐 ( join ‘ 𝑘 ) 𝑎 ) ) }