Metamath Proof Explorer

Definition df-glb

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

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

Detailed syntax breakdown

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