This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvlatl

Description: An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012)

Ref Expression
Assertion cvlatl ⊢ K ∈ CvLat → K ∈ AtLat

Proof

Step Hyp Ref Expression
1 eqid ⊢ Base K = Base K
2 eqid ⊢ ≤ K = ≤ K
3 eqid ⊢ join ⁡ K = join ⁡ K
4 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
5 1 2 3 4 iscvlat ⊢ K ∈ CvLat ↔ K ∈ AtLat ∧ ∀ p ∈ Atoms ⁡ K ∀ q ∈ Atoms ⁡ K ∀ x ∈ Base K ¬ p ≤ K x ∧ p ≤ K x join ⁡ K q → q ≤ K x join ⁡ K p
6 5 simplbi ⊢ K ∈ CvLat → K ∈ AtLat