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 \in V ⟼ {(s \in 𝒫 {Base}_{p} ⟼ (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)))) ↾}_{\{s \| \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))\}})$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		club	$class lub$
1		vp	$setvar p$
2		cvv	$class V$
3		vs	$setvar s$
4		cbs	$class Base$
5	1	cv	$setvar p$
6	5 4	cfv	$class {Base}_{p}$
7	6	cpw	$class 𝒫 {Base}_{p}$
8		vx	$setvar x$
9		vy	$setvar y$
10	3	cv	$setvar s$
11	9	cv	$setvar y$
12		cple	$class le$
13	5 12	cfv	$class \leq_{p}$
14	8	cv	$setvar x$
15	11 14 13	wbr	$wff y \leq_{p} x$
16	15 9 10	wral	$wff \forall y \in s y \leq_{p} x$
17		vz	$setvar z$
18	17	cv	$setvar z$
19	11 18 13	wbr	$wff y \leq_{p} z$
20	19 9 10	wral	$wff \forall y \in s y \leq_{p} z$
21	14 18 13	wbr	$wff x \leq_{p} z$
22	20 21	wi	$wff (\forall y \in s y \leq_{p} z \to x \leq_{p} z)$
23	22 17 6	wral	$wff \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)$
24	16 23	wa	$wff (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))$
25	24 8 6	crio	$class (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)))$
26	3 7 25	cmpt	$class (s \in 𝒫 {Base}_{p} ⟼ (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))))$
27	24 8 6	wreu	$wff \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))$
28	27 3	cab	$class \{s \| \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))\}$
29	26 28	cres	$class ({(s \in 𝒫 {Base}_{p} ⟼ (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)))) ↾}_{\{s \| \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))\}})$
30	1 2 29	cmpt	$class (p \in V ⟼ {(s \in 𝒫 {Base}_{p} ⟼ (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)))) ↾}_{\{s \| \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))\}})$
31	0 30	wceq	$wff lub = (p \in V ⟼ {(s \in 𝒫 {Base}_{p} ⟼ (ι x \in {Base}_{p} \| (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z)))) ↾}_{\{s \| \exists! x \in {Base}_{p} (\forall y \in s y \leq_{p} x \land \forall z \in {Base}_{p} (\forall y \in s y \leq_{p} z \to x \leq_{p} z))\}})$

Metamath Proof Explorer

Definition df-lub

Detailed syntax breakdown