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 e. CvLat -> K e. AtLat )

Proof

Step Hyp Ref Expression
1 eqid
 |-  ( Base ` K ) = ( Base ` K )
2 eqid
 |-  ( le ` K ) = ( le ` K )
3 eqid
 |-  ( join ` K ) = ( join ` K )
4 eqid
 |-  ( Atoms ` K ) = ( Atoms ` K )
5 1 2 3 4 iscvlat
 |-  ( K e. CvLat <-> ( K e. AtLat /\ A. p e. ( Atoms ` K ) A. q e. ( Atoms ` K ) A. x e. ( Base ` K ) ( ( -. p ( le ` K ) x /\ p ( le ` K ) ( x ( join ` K ) q ) ) -> q ( le ` K ) ( x ( join ` K ) p ) ) ) )
6 5 simplbi
 |-  ( K e. CvLat -> K e. AtLat )