Theorem clatpos

Description: A complete lattice is a poset. (Contributed by NM, 8-Sep-2018)

	Ref	Expression
Assertion	clatpos	⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Poset )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
2		eqid	⊢ ( lub ‘ 𝐾 ) = ( lub ‘ 𝐾 )
3		eqid	⊢ ( glb ‘ 𝐾 ) = ( glb ‘ 𝐾 )
4	1 2 3	isclat	⊢ ( 𝐾 ∈ CLat ↔ ( 𝐾 ∈ Poset ∧ ( dom ( lub ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ∧ dom ( glb ‘ 𝐾 ) = 𝒫 ( Base ‘ 𝐾 ) ) ) )
5	4	simplbi	⊢ ( 𝐾 ∈ CLat → 𝐾 ∈ Poset )