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

Definition df-clat 16305
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 16304 . 2  class  CLat
2 vp . . . . . . . 8  setvar  p
32cv 1436 . . . . . . 7  class  p
4 club 16138 . . . . . . 7  class  lub
53, 4cfv 5601 . . . . . 6  class  ( lub `  p )
65cdm 4854 . . . . 5  class  dom  ( lub `  p )
7 cbs 15084 . . . . . . 7  class  Base
83, 7cfv 5601 . . . . . 6  class  ( Base `  p )
98cpw 3985 . . . . 5  class  ~P ( Base `  p )
106, 9wceq 1437 . . . 4  wff  dom  ( lub `  p )  =  ~P ( Base `  p
)
11 cglb 16139 . . . . . . 7  class  glb
123, 11cfv 5601 . . . . . 6  class  ( glb `  p )
1312cdm 4854 . . . . 5  class  dom  ( glb `  p )
1413, 9wceq 1437 . . . 4  wff  dom  ( glb `  p )  =  ~P ( Base `  p
)
1510, 14wa 370 . . 3  wff  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) )
16 cpo 16136 . . 3  class  Poset
1715, 2, 16crab 2786 . 2  class  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }
181, 17wceq 1437 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  16306
  Copyright terms: Public domain W3C validator