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

Definition df-lub 17700
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 17668 . 2 class lub
2 vp . . 3 setvar 𝑝
3 cvv 3398 . . 3 class V
4 vs . . . . 5 setvar 𝑠
52cv 1541 . . . . . . 7 class 𝑝
6 cbs 16586 . . . . . . 7 class Base
75, 6cfv 6339 . . . . . 6 class (Base‘𝑝)
87cpw 4488 . . . . 5 class 𝒫 (Base‘𝑝)
9 vy . . . . . . . . . 10 setvar 𝑦
109cv 1541 . . . . . . . . 9 class 𝑦
11 vx . . . . . . . . . 10 setvar 𝑥
1211cv 1541 . . . . . . . . 9 class 𝑥
13 cple 16675 . . . . . . . . . 10 class le
145, 13cfv 6339 . . . . . . . . 9 class (le‘𝑝)
1510, 12, 14wbr 5030 . . . . . . . 8 wff 𝑦(le‘𝑝)𝑥
164cv 1541 . . . . . . . 8 class 𝑠
1715, 9, 16wral 3053 . . . . . . 7 wff 𝑦𝑠 𝑦(le‘𝑝)𝑥
18 vz . . . . . . . . . . . 12 setvar 𝑧
1918cv 1541 . . . . . . . . . . 11 class 𝑧
2010, 19, 14wbr 5030 . . . . . . . . . 10 wff 𝑦(le‘𝑝)𝑧
2120, 9, 16wral 3053 . . . . . . . . 9 wff 𝑦𝑠 𝑦(le‘𝑝)𝑧
2212, 19, 14wbr 5030 . . . . . . . . 9 wff 𝑥(le‘𝑝)𝑧
2321, 22wi 4 . . . . . . . 8 wff (∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)
2423, 18, 7wral 3053 . . . . . . 7 wff 𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)
2517, 24wa 399 . . . . . 6 wff (∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))
2625, 11, 7crio 7126 . . . . 5 class (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))
274, 8, 26cmpt 5110 . . . 4 class (𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))))
2825, 11, 7wreu 3055 . . . . 5 wff ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))
2928, 4cab 2716 . . . 4 class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))}
3027, 29cres 5527 . . 3 class ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))})
312, 3, 30cmpt 5110 . 2 class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑥 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑦(le‘𝑝)𝑧𝑥(le‘𝑝)𝑧))}))
321, 31wceq 1542 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  17704
  Copyright terms: Public domain W3C validator