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

Definition df-latalg 25182
Description: Algebraic definition of a lattice.  j is called the join of the lattice (and is denoted by 
\/ in textbooks) ,  m is called the meet (and is denoted by 
/\ in textbooks). (Contributed by FL, 11-Dec-2009.)
Assertion
Ref Expression
df-latalg  |-  LatAlg  =  { <. j ,  m >.  |  E. t ( j : ( t  X.  t ) --> t  /\  m : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  (
( x j y )  =  ( y j x )  /\  ( x m y )  =  ( y m x )  /\  ( ( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) ) ) }
Distinct variable group:    j, m, t, x, y, z

Detailed syntax breakdown of Definition df-latalg
StepHypRef Expression
1 clatalg 25181 . 2  class  LatAlg
2 vt . . . . . . . 8  set  t
32cv 1622 . . . . . . 7  class  t
43, 3cxp 4687 . . . . . 6  class  ( t  X.  t )
5 vj . . . . . . 7  set  j
65cv 1622 . . . . . 6  class  j
74, 3, 6wf 5251 . . . . 5  wff  j : ( t  X.  t
) --> t
8 vm . . . . . . 7  set  m
98cv 1622 . . . . . 6  class  m
104, 3, 9wf 5251 . . . . 5  wff  m : ( t  X.  t
) --> t
11 vx . . . . . . . . . . 11  set  x
1211cv 1622 . . . . . . . . . 10  class  x
13 vy . . . . . . . . . . 11  set  y
1413cv 1622 . . . . . . . . . 10  class  y
1512, 14, 6co 5858 . . . . . . . . 9  class  ( x j y )
1614, 12, 6co 5858 . . . . . . . . 9  class  ( y j x )
1715, 16wceq 1623 . . . . . . . 8  wff  ( x j y )  =  ( y j x )
1812, 14, 9co 5858 . . . . . . . . 9  class  ( x m y )
1914, 12, 9co 5858 . . . . . . . . 9  class  ( y m x )
2018, 19wceq 1623 . . . . . . . 8  wff  ( x m y )  =  ( y m x )
2112, 15, 9co 5858 . . . . . . . . . 10  class  ( x m ( x j y ) )
2221, 12wceq 1623 . . . . . . . . 9  wff  ( x m ( x j y ) )  =  x
2312, 18, 6co 5858 . . . . . . . . . 10  class  ( x j ( x m y ) )
2423, 12wceq 1623 . . . . . . . . 9  wff  ( x j ( x m y ) )  =  x
25 vz . . . . . . . . . . . . . . 15  set  z
2625cv 1622 . . . . . . . . . . . . . 14  class  z
2714, 26, 9co 5858 . . . . . . . . . . . . 13  class  ( y m z )
2812, 27, 9co 5858 . . . . . . . . . . . 12  class  ( x m ( y m z ) )
2918, 26, 9co 5858 . . . . . . . . . . . 12  class  ( ( x m y ) m z )
3028, 29wceq 1623 . . . . . . . . . . 11  wff  ( x m ( y m z ) )  =  ( ( x m y ) m z )
3114, 26, 6co 5858 . . . . . . . . . . . . 13  class  ( y j z )
3212, 31, 6co 5858 . . . . . . . . . . . 12  class  ( x j ( y j z ) )
3315, 26, 6co 5858 . . . . . . . . . . . 12  class  ( ( x j y ) j z )
3432, 33wceq 1623 . . . . . . . . . . 11  wff  ( x j ( y j z ) )  =  ( ( x j y ) j z )
3530, 34wa 358 . . . . . . . . . 10  wff  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  (
x j ( y j z ) )  =  ( ( x j y ) j z ) )
3635, 25, 3wral 2543 . . . . . . . . 9  wff  A. z  e.  t  ( (
x m ( y m z ) )  =  ( ( x m y ) m z )  /\  (
x j ( y j z ) )  =  ( ( x j y ) j z ) )
3722, 24, 36w3a 934 . . . . . . . 8  wff  ( ( x m ( x j y ) )  =  x  /\  (
x j ( x m y ) )  =  x  /\  A. z  e.  t  (
( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) )
3817, 20, 37w3a 934 . . . . . . 7  wff  ( ( x j y )  =  ( y j x )  /\  (
x m y )  =  ( y m x )  /\  (
( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) )
3938, 13, 3wral 2543 . . . . . 6  wff  A. y  e.  t  ( (
x j y )  =  ( y j x )  /\  (
x m y )  =  ( y m x )  /\  (
( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) )
4039, 11, 3wral 2543 . . . . 5  wff  A. x  e.  t  A. y  e.  t  ( (
x j y )  =  ( y j x )  /\  (
x m y )  =  ( y m x )  /\  (
( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) )
417, 10, 40w3a 934 . . . 4  wff  ( j : ( t  X.  t ) --> t  /\  m : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  (
( x j y )  =  ( y j x )  /\  ( x m y )  =  ( y m x )  /\  ( ( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) ) )
4241, 2wex 1528 . . 3  wff  E. t
( j : ( t  X.  t ) --> t  /\  m : ( t  X.  t
) --> t  /\  A. x  e.  t  A. y  e.  t  (
( x j y )  =  ( y j x )  /\  ( x m y )  =  ( y m x )  /\  ( ( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) ) )
4342, 5, 8copab 4076 . 2  class  { <. j ,  m >.  |  E. t ( j : ( t  X.  t
) --> t  /\  m : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  (
( x j y )  =  ( y j x )  /\  ( x m y )  =  ( y m x )  /\  ( ( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) ) ) }
441, 43wceq 1623 1  wff  LatAlg  =  { <. j ,  m >.  |  E. t ( j : ( t  X.  t ) --> t  /\  m : ( t  X.  t ) --> t  /\  A. x  e.  t  A. y  e.  t  (
( x j y )  =  ( y j x )  /\  ( x m y )  =  ( y m x )  /\  ( ( x m ( x j y ) )  =  x  /\  ( x j ( x m y ) )  =  x  /\  A. z  e.  t  ( ( x m ( y m z ) )  =  ( ( x m y ) m z )  /\  ( x j ( y j z ) )  =  ( ( x j y ) j z ) ) ) ) ) }
Colors of variables: wff set class
This definition is referenced by:  islatalg  25183
  Copyright terms: Public domain W3C validator