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

Definition df-glb 14109
Description: Define poset greatest lower bound. (Contributed by NM, 19-Jul-2012.)
Assertion
Ref Expression
df-glb  |-  glb  =  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  (
Base `  p )
( A. y  e.  s  x ( le
`  p ) y  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x ) ) ) ) )
Distinct variable group:    s, p, x, y, z

Detailed syntax breakdown of Definition df-glb
StepHypRef Expression
1 cglb 14077 . 2  class  glb
2 vp . . 3  set  p
3 cvv 2788 . . 3  class  _V
4 vs . . . 4  set  s
52cv 1622 . . . . . 6  class  p
6 cbs 13148 . . . . . 6  class  Base
75, 6cfv 5255 . . . . 5  class  ( Base `  p )
87cpw 3625 . . . 4  class  ~P ( Base `  p )
9 vx . . . . . . . . 9  set  x
109cv 1622 . . . . . . . 8  class  x
11 vy . . . . . . . . 9  set  y
1211cv 1622 . . . . . . . 8  class  y
13 cple 13215 . . . . . . . . 9  class  le
145, 13cfv 5255 . . . . . . . 8  class  ( le
`  p )
1510, 12, 14wbr 4023 . . . . . . 7  wff  x ( le `  p ) y
164cv 1622 . . . . . . 7  class  s
1715, 11, 16wral 2543 . . . . . 6  wff  A. y  e.  s  x ( le `  p ) y
18 vz . . . . . . . . . . 11  set  z
1918cv 1622 . . . . . . . . . 10  class  z
2019, 12, 14wbr 4023 . . . . . . . . 9  wff  z ( le `  p ) y
2120, 11, 16wral 2543 . . . . . . . 8  wff  A. y  e.  s  z ( le `  p ) y
2219, 10, 14wbr 4023 . . . . . . . 8  wff  z ( le `  p ) x
2321, 22wi 4 . . . . . . 7  wff  ( A. y  e.  s  z
( le `  p
) y  ->  z
( le `  p
) x )
2423, 18, 7wral 2543 . . . . . 6  wff  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x )
2517, 24wa 358 . . . . 5  wff  ( A. y  e.  s  x
( le `  p
) y  /\  A. z  e.  ( Base `  p ) ( A. y  e.  s  z
( le `  p
) y  ->  z
( le `  p
) x ) )
2625, 9, 7crio 6297 . . . 4  class  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  x ( le `  p ) y  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x ) ) )
274, 8, 26cmpt 4077 . . 3  class  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  x ( le `  p ) y  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x ) ) ) )
282, 3, 27cmpt 4077 . 2  class  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  x ( le `  p ) y  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x ) ) ) ) )
291, 28wceq 1623 1  wff  glb  =  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  (
Base `  p )
( A. y  e.  s  x ( le
`  p ) y  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  z ( le `  p ) y  ->  z ( le
`  p ) x ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  glbfval  14117
  Copyright terms: Public domain W3C validator