Definition df-lub 16797

Description: Define the least upper bound (LUB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 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 = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))

Distinct variable group:   𝑠,𝑝,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-lub

Step	Hyp	Ref	Expression
1		club 16765	. 2 class lub
2		vp	. . 3 setvar 𝑝
3		cvv 3173	. . 3 class V
4		vs	. . . . 5 setvar 𝑠
5	2	cv 1474	. . . . . . 7 class 𝑝
6		cbs 15695	. . . . . . 7 class Base
7	5, 6	cfv 5804	. . . . . 6 class (Base‘𝑝)
8	7	cpw 4108	. . . . 5 class 𝒫 (Base‘𝑝)
9		vy	. . . . . . . . . 10 setvar 𝑦
10	9	cv 1474	. . . . . . . . 9 class 𝑦
11		vx	. . . . . . . . . 10 setvar 𝑥
12	11	cv 1474	. . . . . . . . 9 class 𝑥
13		cple 15775	. . . . . . . . . 10 class le
14	5, 13	cfv 5804	. . . . . . . . 9 class (le‘𝑝)
15	10, 12, 14	wbr 4583	. . . . . . . 8 wff 𝑦(le‘𝑝)𝑥
16	4	cv 1474	. . . . . . . 8 class 𝑠
17	15, 9, 16	wral 2896	. . . . . . 7 wff ∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥
18		vz	. . . . . . . . . . . 12 setvar 𝑧
19	18	cv 1474	. . . . . . . . . . 11 class 𝑧
20	10, 19, 14	wbr 4583	. . . . . . . . . 10 wff 𝑦(le‘𝑝)𝑧
21	20, 9, 16	wral 2896	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧
22	12, 19, 14	wbr 4583	. . . . . . . . 9 wff 𝑥(le‘𝑝)𝑧
23	21, 22	wi 4	. . . . . . . 8 wff (∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)
24	23, 18, 7	wral 2896	. . . . . . 7 wff ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)
25	17, 24	wa 383	. . . . . 6 wff (∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))
26	25, 11, 7	crio 6510	. . . . 5 class (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))
27	4, 8, 26	cmpt 4643	. . . 4 class (𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))))
28	25, 11, 7	wreu 2898	. . . . 5 wff ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))
29	28, 4	cab 2596	. . . 4 class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}
30	27, 29	cres 5040	. . 3 class ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})
31	2, 3, 30	cmpt 4643	. 2 class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))
32	1, 31	wceq 1475	1 wff lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))

This definition is referenced by:  lubfval  16801