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

Definition df-clat 15717
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 15716 . 2  class  CLat
2 vp . . . . . . . 8  setvar  p
32cv 1382 . . . . . . 7  class  p
4 club 15550 . . . . . . 7  class  lub
53, 4cfv 5578 . . . . . 6  class  ( lub `  p )
65cdm 4989 . . . . 5  class  dom  ( lub `  p )
7 cbs 14614 . . . . . . 7  class  Base
83, 7cfv 5578 . . . . . 6  class  ( Base `  p )
98cpw 3997 . . . . 5  class  ~P ( Base `  p )
106, 9wceq 1383 . . . 4  wff  dom  ( lub `  p )  =  ~P ( Base `  p
)
11 cglb 15551 . . . . . . 7  class  glb
123, 11cfv 5578 . . . . . 6  class  ( glb `  p )
1312cdm 4989 . . . . 5  class  dom  ( glb `  p )
1413, 9wceq 1383 . . . 4  wff  dom  ( glb `  p )  =  ~P ( Base `  p
)
1510, 14wa 369 . . 3  wff  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) )
16 cpo 15548 . . 3  class  Poset
1715, 2, 16crab 2797 . 2  class  { p  e.  Poset  |  ( dom  ( lub `  p
)  =  ~P ( Base `  p )  /\  dom  ( glb `  p
)  =  ~P ( Base `  p ) ) }
181, 17wceq 1383 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  15718
  Copyright terms: Public domain W3C validator