Metamath Proof Explorer

Definition df-lub

Description: Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets s for which the LUB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011) (Revised by NM, 6-Sep-2018)

Ref Expression
Assertion 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 ) ) ) ) |` { s | E! 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 ) ) } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 club 
 |-  lub
1 vp 
 |-  p
2 cvv 
 |-  _V
3 vs 
 |-  s
4 cbs 
 |-  Base
5 1 cv 
 |-  p
6 5 4 cfv 
 |-  ( Base ` p )
7 6 cpw 
 |-  ~P ( Base ` p )
8 vx 
 |-  x
9 vy 
 |-  y
10 3 cv 
 |-  s
11 9 cv 
 |-  y
12 cple 
 |-  le
13 5 12 cfv 
 |-  ( le ` p )
14 8 cv 
 |-  x
15 11 14 13 wbr 
 |-  y ( le ` p ) x
16 15 9 10 wral 
 |-  A. y e. s y ( le ` p ) x
17 vz 
 |-  z
18 17 cv 
 |-  z
19 11 18 13 wbr 
 |-  y ( le ` p ) z
20 19 9 10 wral 
 |-  A. y e. s y ( le ` p ) z
21 14 18 13 wbr 
 |-  x ( le ` p ) z
22 20 21 wi 
 |-  ( A. y e. s y ( le ` p ) z -> x ( le ` p ) z )
23 22 17 6 wral 
 |-  A. z e. ( Base ` p ) ( A. y e. s y ( le ` p ) z -> x ( le ` p ) z )
24 16 23 wa 
 |-  ( 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 ) )
25 24 8 6 crio 
 |-  ( 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 ) ) )
26 3 7 25 cmpt 
 |-  ( 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 ) ) ) )
27 24 8 6 wreu 
 |-  E! 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 ) )
28 27 3 cab 
 |-  { s | E! 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 ) ) }
29 26 28 cres 
 |-  ( ( 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 ) ) ) ) |` { s | E! 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 ) ) } )
30 1 2 29 cmpt 
 |-  ( 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 ) ) ) ) |` { s | E! 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 ) ) } ) )
31 0 30 wceq 
 |-  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 ) ) ) ) |` { s | E! 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 ) ) } ) )