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

Definition df-clat 14210
Description: Define the class of all complete lattices. (Contributed by NM, 18-Oct-2012.)
Assertion
Ref Expression
df-clat  |-  CLat  =  { p  e.  Poset  |  A. s ( s  C_  ( Base `  p )  ->  ( ( ( lub `  p ) `  s
)  e.  ( Base `  p )  /\  (
( glb `  p
) `  s )  e.  ( Base `  p
) ) ) }
Distinct variable group:    s, p

Detailed syntax breakdown of Definition df-clat
StepHypRef Expression
1 ccla 14209 . 2  class  CLat
2 vs . . . . . . 7  set  s
32cv 1622 . . . . . 6  class  s
4 vp . . . . . . . 8  set  p
54cv 1622 . . . . . . 7  class  p
6 cbs 13144 . . . . . . 7  class  Base
75, 6cfv 5221 . . . . . 6  class  ( Base `  p )
83, 7wss 3153 . . . . 5  wff  s  C_  ( Base `  p )
9 club 14072 . . . . . . . . 9  class  lub
105, 9cfv 5221 . . . . . . . 8  class  ( lub `  p )
113, 10cfv 5221 . . . . . . 7  class  ( ( lub `  p ) `
 s )
1211, 7wcel 1685 . . . . . 6  wff  ( ( lub `  p ) `
 s )  e.  ( Base `  p
)
13 cglb 14073 . . . . . . . . 9  class  glb
145, 13cfv 5221 . . . . . . . 8  class  ( glb `  p )
153, 14cfv 5221 . . . . . . 7  class  ( ( glb `  p ) `
 s )
1615, 7wcel 1685 . . . . . 6  wff  ( ( glb `  p ) `
 s )  e.  ( Base `  p
)
1712, 16wa 358 . . . . 5  wff  ( ( ( lub `  p
) `  s )  e.  ( Base `  p
)  /\  ( ( glb `  p ) `  s )  e.  (
Base `  p )
)
188, 17wi 4 . . . 4  wff  ( s 
C_  ( Base `  p
)  ->  ( (
( lub `  p
) `  s )  e.  ( Base `  p
)  /\  ( ( glb `  p ) `  s )  e.  (
Base `  p )
) )
1918, 2wal 1527 . . 3  wff  A. s
( s  C_  ( Base `  p )  -> 
( ( ( lub `  p ) `  s
)  e.  ( Base `  p )  /\  (
( glb `  p
) `  s )  e.  ( Base `  p
) ) )
20 cpo 14070 . . 3  class  Poset
2119, 4, 20crab 2548 . 2  class  { p  e.  Poset  |  A. s
( s  C_  ( Base `  p )  -> 
( ( ( lub `  p ) `  s
)  e.  ( Base `  p )  /\  (
( glb `  p
) `  s )  e.  ( Base `  p
) ) ) }
221, 21wceq 1623 1  wff  CLat  =  { p  e.  Poset  |  A. s ( s  C_  ( Base `  p )  ->  ( ( ( lub `  p ) `  s
)  e.  ( Base `  p )  /\  (
( glb `  p
) `  s )  e.  ( Base `  p
) ) ) }
Colors of variables: wff set class
This definition is referenced by:  isclat  14211
  Copyright terms: Public domain W3C validator