Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnlat Unicode version

Definition df-bnlat 25400
Description: A bound lattice is a lattice that has the greatest and the least element. (Contributed by FL, 21-May-2012.)
Assertion
Ref Expression
df-bnlat  |-  BndLat  =  {
r  e.  LatRel  |  ( (leR `  r )  e.  dom  r  /\  ( ge `  r )  e. 
dom  r ) }

Detailed syntax breakdown of Definition df-bnlat
StepHypRef Expression
1 clbl 25399 . 2  class  BndLat
2 vr . . . . . . 7  set  r
32cv 1631 . . . . . 6  class  r
4 cse 25324 . . . . . 6  class leR
53, 4cfv 5271 . . . . 5  class  (leR `  r )
63cdm 4705 . . . . 5  class  dom  r
75, 6wcel 1696 . . . 4  wff  (leR `  r )  e.  dom  r
8 cge 25323 . . . . . 6  class  ge
93, 8cfv 5271 . . . . 5  class  ( ge
`  r )
109, 6wcel 1696 . . . 4  wff  ( ge
`  r )  e. 
dom  r
117, 10wa 358 . . 3  wff  ( (leR
`  r )  e. 
dom  r  /\  ( ge `  r )  e. 
dom  r )
12 cla 14321 . . 3  class  LatRel
1311, 2, 12crab 2560 . 2  class  { r  e.  LatRel  |  ( (leR
`  r )  e. 
dom  r  /\  ( ge `  r )  e. 
dom  r ) }
141, 13wceq 1632 1  wff  BndLat  =  {
r  e.  LatRel  |  ( (leR `  r )  e.  dom  r  /\  ( ge `  r )  e. 
dom  r ) }
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator