Definition df-lub 16974

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

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

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

Detailed syntax breakdown of Definition df-lub

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

This definition is referenced by:  lubfval  16978