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 )