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 ) ) } ) )