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

Definition df-clat 16402
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 16401 . 2  class  CLat
2 vp . . . . . . . 8  setvar  p
32cv 1453 . . . . . . 7  class  p
4 club 16235 . . . . . . 7  class  lub
53, 4cfv 5600 . . . . . 6  class  ( lub `  p )
65cdm 4852 . . . . 5  class  dom  ( lub `  p )
7 cbs 15169 . . . . . . 7  class  Base
83, 7cfv 5600 . . . . . 6  class  ( Base `  p )
98cpw 3962 . . . . 5  class  ~P ( Base `  p )
106, 9wceq 1454 . . . 4  wff  dom  ( lub `  p )  =  ~P ( Base `  p
)
11 cglb 16236 . . . . . . 7  class  glb
123, 11cfv 5600 . . . . . 6  class  ( glb `  p )
1312cdm 4852 . . . . 5  class  dom  ( glb `  p )
1413, 9wceq 1454 . . . 4  wff  dom  ( glb `  p )  =  ~P ( Base `  p
)
1510, 14wa 375 . . 3  wff  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) )
16 cpo 16233 . . 3  class  Poset
1715, 2, 16crab 2752 . 2  class  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }
181, 17wceq 1454 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  16403
  Copyright terms: Public domain W3C validator