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

Definition df-drs 16850
Description: Define the class of directed sets. A directed set is a nonempty preordered set where every pair of elements have some upper bound. Note that it is not required that there exist a least upper bound.

There is no consensus in the literature over whether directed sets are allowed to be empty. It is slightly more convenient for us if they are not. (Contributed by Stefan O'Rear, 1-Feb-2015.)

Assertion
Ref Expression
df-drs Dirset = {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-drs
StepHypRef Expression
1 cdrs 16848 . 2 class Dirset
2 vb . . . . . . . 8 setvar 𝑏
32cv 1479 . . . . . . 7 class 𝑏
4 c0 3891 . . . . . . 7 class
53, 4wne 2790 . . . . . 6 wff 𝑏 ≠ ∅
6 vx . . . . . . . . . . . 12 setvar 𝑥
76cv 1479 . . . . . . . . . . 11 class 𝑥
8 vz . . . . . . . . . . . 12 setvar 𝑧
98cv 1479 . . . . . . . . . . 11 class 𝑧
10 vr . . . . . . . . . . . 12 setvar 𝑟
1110cv 1479 . . . . . . . . . . 11 class 𝑟
127, 9, 11wbr 4613 . . . . . . . . . 10 wff 𝑥𝑟𝑧
13 vy . . . . . . . . . . . 12 setvar 𝑦
1413cv 1479 . . . . . . . . . . 11 class 𝑦
1514, 9, 11wbr 4613 . . . . . . . . . 10 wff 𝑦𝑟𝑧
1612, 15wa 384 . . . . . . . . 9 wff (𝑥𝑟𝑧𝑦𝑟𝑧)
1716, 8, 3wrex 2908 . . . . . . . 8 wff 𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
1817, 13, 3wral 2907 . . . . . . 7 wff 𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
1918, 6, 3wral 2907 . . . . . 6 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
205, 19wa 384 . . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
21 vf . . . . . . 7 setvar 𝑓
2221cv 1479 . . . . . 6 class 𝑓
23 cple 15869 . . . . . 6 class le
2422, 23cfv 5847 . . . . 5 class (le‘𝑓)
2520, 10, 24wsbc 3417 . . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
26 cbs 15781 . . . . 5 class Base
2722, 26cfv 5847 . . . 4 class (Base‘𝑓)
2825, 2, 27wsbc 3417 . . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
29 cpreset 16847 . . 3 class Preset
3028, 21, 29crab 2911 . 2 class {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
311, 30wceq 1480 1 wff Dirset = {𝑓 ∈ Preset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isdrs  16855
  Copyright terms: Public domain W3C validator