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

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-glb

Detailed syntax breakdown