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

Definition df-lub 14108
Description: Define poset least upper bound. If it doesn't exist, an undefined value not in the base set is returned. (Contributed by NM, 12-Sep-2011.)
Assertion
Ref Expression
df-lub  |-  lub  =  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  (
Base `  p )
( A. y  e.  s  y ( le
`  p ) x  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z ) ) ) ) )
Distinct variable group:    s, p, x, y, z

Detailed syntax breakdown of Definition df-lub
StepHypRef Expression
1 club 14076 . 2  class  lub
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 vy . . . . . . . . 9  set  y
109cv 1622 . . . . . . . 8  class  y
11 vx . . . . . . . . 9  set  x
1211cv 1622 . . . . . . . 8  class  x
13 cple 13215 . . . . . . . . 9  class  le
145, 13cfv 5255 . . . . . . . 8  class  ( le
`  p )
1510, 12, 14wbr 4023 . . . . . . 7  wff  y ( le `  p ) x
164cv 1622 . . . . . . 7  class  s
1715, 9, 16wral 2543 . . . . . 6  wff  A. y  e.  s  y ( le `  p ) x
18 vz . . . . . . . . . . 11  set  z
1918cv 1622 . . . . . . . . . 10  class  z
2010, 19, 14wbr 4023 . . . . . . . . 9  wff  y ( le `  p ) z
2120, 9, 16wral 2543 . . . . . . . 8  wff  A. y  e.  s  y ( le `  p ) z
2212, 19, 14wbr 4023 . . . . . . . 8  wff  x ( le `  p ) z
2321, 22wi 4 . . . . . . 7  wff  ( A. y  e.  s  y
( le `  p
) z  ->  x
( le `  p
) z )
2423, 18, 7wral 2543 . . . . . 6  wff  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z )
2517, 24wa 358 . . . . 5  wff  ( A. y  e.  s  y
( le `  p
) x  /\  A. z  e.  ( Base `  p ) ( A. y  e.  s  y
( le `  p
) z  ->  x
( le `  p
) z ) )
2625, 11, 7crio 6297 . . . 4  class  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) x  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z ) ) )
274, 8, 26cmpt 4077 . . 3  class  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) x  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z ) ) ) )
282, 3, 27cmpt 4077 . 2  class  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) x  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z ) ) ) ) )
291, 28wceq 1623 1  wff  lub  =  ( p  e.  _V  |->  ( s  e.  ~P ( Base `  p )  |->  ( iota_ x  e.  (
Base `  p )
( A. y  e.  s  y ( le
`  p ) x  /\  A. z  e.  ( Base `  p
) ( A. y  e.  s  y ( le `  p ) z  ->  x ( le
`  p ) z ) ) ) ) )
Colors of variables: wff set class
This definition is referenced by:  lubfval  14112
  Copyright terms: Public domain W3C validator