Definition df-glb 16975

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

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

Distinct variable group:   s, p, x, y, z

Detailed syntax breakdown of Definition df-glb

Step	Hyp	Ref	Expression
1		cglb 16943	. 2 class glb
2		vp	. . 3 setvar p
3		cvv 3200	. . 3 class _V
4		vs	. . . . 5 setvar s
5	2	cv 1482	. . . . . . 7 class p
6		cbs 15857	. . . . . . 7 class Base
7	5, 6	cfv 5888	. . . . . 6 class ( Base ` p )
8	7	cpw 4158	. . . . 5 class ~P ( Base ` p )
9		vx	. . . . . . . . . 10 setvar x
10	9	cv 1482	. . . . . . . . 9 class x
11		vy	. . . . . . . . . 10 setvar y
12	11	cv 1482	. . . . . . . . 9 class y
13		cple 15948	. . . . . . . . . 10 class le
14	5, 13	cfv 5888	. . . . . . . . 9 class ( le ` p )
15	10, 12, 14	wbr 4653	. . . . . . . 8 wff x ( le ` p ) y
16	4	cv 1482	. . . . . . . 8 class s
17	15, 11, 16	wral 2912	. . . . . . 7 wff A. y e. s x ( le ` p ) y
18		vz	. . . . . . . . . . . 12 setvar z
19	18	cv 1482	. . . . . . . . . . 11 class z
20	19, 12, 14	wbr 4653	. . . . . . . . . 10 wff z ( le ` p ) y
21	20, 11, 16	wral 2912	. . . . . . . . 9 wff A. y e. s z ( le ` p ) y
22	19, 10, 14	wbr 4653	. . . . . . . . 9 wff z ( le ` p ) x
23	21, 22	wi 4	. . . . . . . 8 wff ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x )
24	23, 18, 7	wral 2912	. . . . . . 7 wff A. z e. ( Base ` p ) ( A. y e. s z ( le ` p ) y -> z ( le ` p ) x )
25	17, 24	wa 384	. . . . . 6 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 ) )
26	25, 9, 7	crio 6610	. . . . 5 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 ) ) )
27	4, 8, 26	cmpt 4729	. . . 4 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 ) ) ) )
28	25, 9, 7	wreu 2914	. . . . 5 wff 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	28, 4	cab 2608	. . . 4 class { 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	27, 29	cres 5116	. . 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 ) ) ) ) |` { 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	2, 3, 30	cmpt 4729	. 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 ) ) ) ) |` { 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 ) ) } ) )
32	1, 31	wceq 1483	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 ) ) ) ) |` { 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 ) ) } ) )

This definition is referenced by:  glbfval  16991