Description: An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | atllat | ⊢ ( 𝐾 ∈ AtLat → 𝐾 ∈ Lat ) |
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 ) |