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

Definition df-lar 14326
Description: Define the class of all lattices, which are posets in which every two elements have upper and lower bounds. (Contributed by NM, 12-Jun-2008.)
Assertion
Ref Expression
df-lar  |-  LatRel  =  {
r  e.  PosetRel  |  A. x  e.  dom  r A. y  e.  dom  r ( ( r  sup w  { x ,  y } )  e.  dom  r  /\  ( r  inf
w  { x ,  y } )  e. 
dom  r ) }
Distinct variable group:    x, r, y

Detailed syntax breakdown of Definition df-lar
StepHypRef Expression
1 cla 14321 . 2  class  LatRel
2 vr . . . . . . . . 9  set  r
32cv 1631 . . . . . . . 8  class  r
4 vx . . . . . . . . . 10  set  x
54cv 1631 . . . . . . . . 9  class  x
6 vy . . . . . . . . . 10  set  y
76cv 1631 . . . . . . . . 9  class  y
85, 7cpr 3654 . . . . . . . 8  class  { x ,  y }
9 cspw 14319 . . . . . . . 8  class  sup w
103, 8, 9co 5874 . . . . . . 7  class  ( r  sup w  { x ,  y } )
113cdm 4705 . . . . . . 7  class  dom  r
1210, 11wcel 1696 . . . . . 6  wff  ( r  sup w  { x ,  y } )  e.  dom  r
13 cinf 14320 . . . . . . . 8  class  inf w
143, 8, 13co 5874 . . . . . . 7  class  ( r  inf w  { x ,  y } )
1514, 11wcel 1696 . . . . . 6  wff  ( r  inf w  { x ,  y } )  e.  dom  r
1612, 15wa 358 . . . . 5  wff  ( ( r  sup w  {
x ,  y } )  e.  dom  r  /\  ( r  inf w  { x ,  y } )  e.  dom  r )
1716, 6, 11wral 2556 . . . 4  wff  A. y  e.  dom  r ( ( r  sup w  {
x ,  y } )  e.  dom  r  /\  ( r  inf w  { x ,  y } )  e.  dom  r )
1817, 4, 11wral 2556 . . 3  wff  A. x  e.  dom  r A. y  e.  dom  r ( ( r  sup w  {
x ,  y } )  e.  dom  r  /\  ( r  inf w  { x ,  y } )  e.  dom  r )
19 cps 14317 . . 3  class  PosetRel
2018, 2, 19crab 2560 . 2  class  { r  e.  PosetRel  |  A. x  e.  dom  r A. y  e.  dom  r ( ( r  sup w  {
x ,  y } )  e.  dom  r  /\  ( r  inf w  { x ,  y } )  e.  dom  r ) }
211, 20wceq 1632 1  wff  LatRel  =  {
r  e.  PosetRel  |  A. x  e.  dom  r A. y  e.  dom  r ( ( r  sup w  { x ,  y } )  e.  dom  r  /\  ( r  inf
w  { x ,  y } )  e. 
dom  r ) }
Colors of variables: wff set class
This definition is referenced by:  isla  14358
  Copyright terms: Public domain W3C validator