Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lub Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 club 16765 . 2 class lub
2 vp . . 3 setvar 𝑝
3 cvv 3173 . . 3 class V
4 vs . . . . 5 setvar 𝑠
52cv 1474 . . . . . . 7 class 𝑝
6 cbs 15695 . . . . . . 7 class Base
75, 6cfv 5804 . . . . . 6 class (Base‘𝑝)
87cpw 4108 . . . . 5 class 𝒫 (Base‘𝑝)
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1474 . . . . . . . . 9 class 𝑦
11 vx . . . . . . . . . 10 setvar 𝑥
1211cv 1474 . . . . . . . . 9 class 𝑥
13 cple 15775 . . . . . . . . . 10 class le
145, 13cfv 5804 . . . . . . . . 9 class (le‘𝑝)
1510, 12, 14wbr 4583 . . . . . . . 8 wff 𝑦(le‘𝑝)𝑥
164cv 1474 . . . . . . . 8 class 𝑠
1715, 9, 16wral 2896 . . . . . . 7 wff 𝑦𝑠 𝑦(le‘𝑝)𝑥
18 vz . . . . . . . . . . . 12 setvar 𝑧
1918cv 1474 . . . . . . . . . . 11 class 𝑧
2010, 19, 14wbr 4583 . . . . . . . . . 10 wff 𝑦(le‘𝑝)𝑧
2120, 9, 16wral 2896 . . . . . . . . 9 wff 𝑦𝑠 𝑦(le‘𝑝)𝑧
2212, 19, 14wbr 4583 . . . . . . . . 9 wff 𝑥(le‘𝑝)𝑧
2321, 22wi 4 . . . . . . . 8 wff (∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)
2423, 18, 7wral 2896 . . . . . . 7 wff 𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)
2517, 24wa 383 . . . . . 6 wff (∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))
2625, 11, 7crio 6510 . . . . 5 class (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))
274, 8, 26cmpt 4643 . . . 4 class (𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))))
2825, 11, 7wreu 2898 . . . . 5 wff ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))
2928, 4cab 2596 . . . 4 class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))}
3027, 29cres 5040 . . 3 class ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))})
312, 3, 30cmpt 4643 . 2 class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))}))
321, 31wceq 1475 1 wff lub = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))}))
 Colors of variables: wff setvar class This definition is referenced by:  lubfval  16801
 Copyright terms: Public domain W3C validator