MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clat Structured version   Unicode version

Definition df-clat 15940
Description: Define the class of all complete lattices, where every subset of the base set has an LUB and a GLB. (Contributed by NM, 18-Oct-2012.) (Revised by NM, 12-Sep-2018.)
Assertion
Ref Expression
df-clat  |-  CLat  =  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }

Detailed syntax breakdown of Definition df-clat
StepHypRef Expression
1 ccla 15939 . 2  class  CLat
2 vp . . . . . . . 8  setvar  p
32cv 1397 . . . . . . 7  class  p
4 club 15773 . . . . . . 7  class  lub
53, 4cfv 5570 . . . . . 6  class  ( lub `  p )
65cdm 4988 . . . . 5  class  dom  ( lub `  p )
7 cbs 14719 . . . . . . 7  class  Base
83, 7cfv 5570 . . . . . 6  class  ( Base `  p )
98cpw 3999 . . . . 5  class  ~P ( Base `  p )
106, 9wceq 1398 . . . 4  wff  dom  ( lub `  p )  =  ~P ( Base `  p
)
11 cglb 15774 . . . . . . 7  class  glb
123, 11cfv 5570 . . . . . 6  class  ( glb `  p )
1312cdm 4988 . . . . 5  class  dom  ( glb `  p )
1413, 9wceq 1398 . . . 4  wff  dom  ( glb `  p )  =  ~P ( Base `  p
)
1510, 14wa 367 . . 3  wff  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) )
16 cpo 15771 . . 3  class  Poset
1715, 2, 16crab 2808 . 2  class  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }
181, 17wceq 1398 1  wff  CLat  =  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }
Colors of variables: wff setvar class
This definition is referenced by:  isclat  15941
  Copyright terms: Public domain W3C validator