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

Definition df-lat 14168
Description: Define the class of all lattices. A lattice is a poset in which the join and meet of any two elements always exists. (Contributed by NM, 18-Oct-2012.)
Assertion
Ref Expression
df-lat  |-  Lat  =  { p  e.  Poset  |  A. x  e.  ( Base `  p ) A. y  e.  ( Base `  p
) ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
) }
Distinct variable group:    x, p, y

Detailed syntax breakdown of Definition df-lat
StepHypRef Expression
1 clat 14167 . 2  class  Lat
2 vx . . . . . . . . 9  set  x
32cv 1631 . . . . . . . 8  class  x
4 vy . . . . . . . . 9  set  y
54cv 1631 . . . . . . . 8  class  y
6 vp . . . . . . . . . 10  set  p
76cv 1631 . . . . . . . . 9  class  p
8 cjn 14094 . . . . . . . . 9  class  join
97, 8cfv 5271 . . . . . . . 8  class  ( join `  p )
103, 5, 9co 5874 . . . . . . 7  class  ( x ( join `  p
) y )
11 cbs 13164 . . . . . . . 8  class  Base
127, 11cfv 5271 . . . . . . 7  class  ( Base `  p )
1310, 12wcel 1696 . . . . . 6  wff  ( x ( join `  p
) y )  e.  ( Base `  p
)
14 cmee 14095 . . . . . . . . 9  class  meet
157, 14cfv 5271 . . . . . . . 8  class  ( meet `  p )
163, 5, 15co 5874 . . . . . . 7  class  ( x ( meet `  p
) y )
1716, 12wcel 1696 . . . . . 6  wff  ( x ( meet `  p
) y )  e.  ( Base `  p
)
1813, 17wa 358 . . . . 5  wff  ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
)
1918, 4, 12wral 2556 . . . 4  wff  A. y  e.  ( Base `  p
) ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
)
2019, 2, 12wral 2556 . . 3  wff  A. x  e.  ( Base `  p
) A. y  e.  ( Base `  p
) ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
)
21 cpo 14090 . . 3  class  Poset
2220, 6, 21crab 2560 . 2  class  { p  e.  Poset  |  A. x  e.  ( Base `  p
) A. y  e.  ( Base `  p
) ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
) }
231, 22wceq 1632 1  wff  Lat  =  { p  e.  Poset  |  A. x  e.  ( Base `  p ) A. y  e.  ( Base `  p
) ( ( x ( join `  p
) y )  e.  ( Base `  p
)  /\  ( x
( meet `  p )
y )  e.  (
Base `  p )
) }
Colors of variables: wff set class
This definition is referenced by:  islat  14169
  Copyright terms: Public domain W3C validator