Metamath Proof Explorer

Theorem clatpos

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

Ref Expression
Assertion clatpos 
|- ( K e. CLat -> K e. Poset )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` K ) = ( Base ` K )
2 eqid 
 |-  ( lub ` K ) = ( lub ` K )
3 eqid 
 |-  ( glb ` K ) = ( glb ` K )
4 1 2 3 isclat 
 |-  ( K e. CLat <-> ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) )
5 4 simplbi 
 |-  ( K e. CLat -> K e. Poset )