Metamath Proof Explorer

Theorem atllat

Description: An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011)

Ref Expression
Assertion atllat 
|- ( K e. AtLat -> K e. Lat )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( glb ` K ) = ( glb ` K )
3 eqid 
 |-  ( le ` K ) = ( le ` K )
4 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
5 eqid 
 |-  ( Atoms ` K ) = ( Atoms ` K )
6 1 2 3 4 5 isatl 
 |-  ( K e. AtLat <-> ( K e. Lat /\ ( Base ` K ) e. dom ( glb ` K ) /\ A. x e. ( Base ` K ) ( x =/= ( 0. ` K ) -> E. p e. ( Atoms ` K ) p ( le ` K ) x ) ) )
7 6 simp1bi 
 |-  ( K e. AtLat -> K e. Lat )