Theorem cvlatl

Description: An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012)

	Ref	Expression
Assertion	cvlatl	⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
3		eqid	⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
4		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
5	1 2 3 4	iscvlat	⊢ ( 𝐾 ∈ CvLat ↔ ( 𝐾 ∈ AtLat ∧ ∀ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ∀ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑥 ∧ 𝑝 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑞 ) ) → 𝑞 ( le ‘ 𝐾 ) ( 𝑥 ( join ‘ 𝐾 ) 𝑝 ) ) ) )
6	5	simplbi	⊢ ( 𝐾 ∈ CvLat → 𝐾 ∈ AtLat )