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

Definition df-glb 16747
Description: Define the greatest lower bound (GLB) of a set of (poset) elements. The domain is restricted to exclude sets 𝑠 for which the GLB doesn't exist uniquely. (Contributed by NM, 12-Sep-2011.) (Revised by NM, 6-Sep-2018.)
Assertion
Ref Expression
df-glb glb = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))}))
Distinct variable group:   𝑠,𝑝,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-glb
StepHypRef Expression
1 cglb 16715 . 2 class glb
2 vp . . 3 setvar 𝑝
3 cvv 3172 . . 3 class V
4 vs . . . . 5 setvar 𝑠
52cv 1473 . . . . . . 7 class 𝑝
6 cbs 15644 . . . . . . 7 class Base
75, 6cfv 5790 . . . . . 6 class (Base‘𝑝)
87cpw 4107 . . . . 5 class 𝒫 (Base‘𝑝)
9 vx . . . . . . . . . 10 setvar 𝑥
109cv 1473 . . . . . . . . 9 class 𝑥
11 vy . . . . . . . . . 10 setvar 𝑦
1211cv 1473 . . . . . . . . 9 class 𝑦
13 cple 15724 . . . . . . . . . 10 class le
145, 13cfv 5790 . . . . . . . . 9 class (le‘𝑝)
1510, 12, 14wbr 4577 . . . . . . . 8 wff 𝑥(le‘𝑝)𝑦
164cv 1473 . . . . . . . 8 class 𝑠
1715, 11, 16wral 2895 . . . . . . 7 wff 𝑦𝑠 𝑥(le‘𝑝)𝑦
18 vz . . . . . . . . . . . 12 setvar 𝑧
1918cv 1473 . . . . . . . . . . 11 class 𝑧
2019, 12, 14wbr 4577 . . . . . . . . . 10 wff 𝑧(le‘𝑝)𝑦
2120, 11, 16wral 2895 . . . . . . . . 9 wff 𝑦𝑠 𝑧(le‘𝑝)𝑦
2219, 10, 14wbr 4577 . . . . . . . . 9 wff 𝑧(le‘𝑝)𝑥
2321, 22wi 4 . . . . . . . 8 wff (∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)
2423, 18, 7wral 2895 . . . . . . 7 wff 𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)
2517, 24wa 382 . . . . . 6 wff (∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))
2625, 9, 7crio 6488 . . . . 5 class (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)))
274, 8, 26cmpt 4637 . . . 4 class (𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))))
2825, 9, 7wreu 2897 . . . . 5 wff ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))
2928, 4cab 2595 . . . 4 class {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))}
3027, 29cres 5030 . . 3 class ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))})
312, 3, 30cmpt 4637 . 2 class (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))}))
321, 31wceq 1474 1 wff glb = (𝑝 ∈ V ↦ ((𝑠 ∈ 𝒫 (Base‘𝑝) ↦ (𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥)))) ↾ {𝑠 ∣ ∃!𝑥 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑥(le‘𝑝)𝑦 ∧ ∀𝑧 ∈ (Base‘𝑝)(∀𝑦𝑠 𝑧(le‘𝑝)𝑦𝑧(le‘𝑝)𝑥))}))
Colors of variables: wff setvar class
This definition is referenced by:  glbfval  16763
  Copyright terms: Public domain W3C validator