Metamath Proof Explorer


Theorem atllat

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

Ref Expression
Assertion atllat ( 𝐾 ∈ AtLat → 𝐾 ∈ Lat )

Proof

Step Hyp Ref Expression
1 eqid ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2 eqid ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
3 eqid ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
4 eqid ( 0. ‘ 𝐾 ) = ( 0. ‘ 𝐾 )
5 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
6 1 2 3 4 5 isatl ( 𝐾 ∈ AtLat ↔ ( 𝐾 ∈ Lat ∧ ( Base ‘ 𝐾 ) ∈ dom ( glb ‘ 𝐾 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( 𝑥 ≠ ( 0. ‘ 𝐾 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) 𝑝 ( le ‘ 𝐾 ) 𝑥 ) ) )
7 6 simp1bi ( 𝐾 ∈ AtLat → 𝐾 ∈ Lat )