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 ) |
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 ) |