Definition df-lub 17979

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 17942	. 2 class lub
2		vp	. . 3 setvar 𝑝
3		cvv 3422	. . 3 class V
4		vs	. . . . 5 setvar 𝑠
5	2	cv 1538	. . . . . . 7 class 𝑝
6		cbs 16840	. . . . . . 7 class Base
7	5, 6	cfv 6418	. . . . . 6 class (Base‘𝑝)
8	7	cpw 4530	. . . . 5 class 𝒫 (Base‘𝑝)
9		vy	. . . . . . . . . 10 setvar 𝑦
10	9	cv 1538	. . . . . . . . 9 class 𝑦
11		vx	. . . . . . . . . 10 setvar 𝑥
12	11	cv 1538	. . . . . . . . 9 class 𝑥
13		cple 16895	. . . . . . . . . 10 class le
14	5, 13	cfv 6418	. . . . . . . . 9 class (le‘𝑝)
15	10, 12, 14	wbr 5070	. . . . . . . 8 wff 𝑦(le‘𝑝)𝑥
16	4	cv 1538	. . . . . . . 8 class 𝑠
17	15, 9, 16	wral 3063	. . . . . . 7 wff ∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥
18		vz	. . . . . . . . . . . 12 setvar 𝑧
19	18	cv 1538	. . . . . . . . . . 11 class 𝑧
20	10, 19, 14	wbr 5070	. . . . . . . . . 10 wff 𝑦(le‘𝑝)𝑧
21	20, 9, 16	wral 3063	. . . . . . . . 9 wff ∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧
22	12, 19, 14	wbr 5070	. . . . . . . . 9 wff 𝑥(le‘𝑝)𝑧
23	21, 22	wi 4	. . . . . . . 8 wff (∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)
24	23, 18, 7	wral 3063	. . . . . . 7 wff ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)
25	17, 24	wa 395	. . . . . 6 wff (∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))
26	25, 11, 7	crio 7211	. . . . 5 class (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))
27	4, 8, 26	cmpt 5153	. . . 4 class (𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))))
28	25, 11, 7	wreu 3065	. . . . 5 wff ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))
29	28, 4	cab 2715	. . . 4 class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}
30	27, 29	cres 5582	. . 3 class ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))})
31	2, 3, 30	cmpt 5153	. 2 class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))
32	1, 31	wceq 1539	1 wff lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (℩𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦 ∈ 𝑠 𝑦(le‘𝑝)𝑧 → 𝑥(le‘𝑝)𝑧))}))

This definition is referenced by:  lubfval  17983