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 17534
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 = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
Distinct variable group:   𝑓,𝑏,𝑟,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-drs
StepHypRef Expression
1 cdrs 17532 . 2 class Dirset
2 vb . . . . . . . 8 setvar 𝑏
32cv 1537 . . . . . . 7 class 𝑏
4 c0 4246 . . . . . . 7 class
53, 4wne 2990 . . . . . 6 wff 𝑏 ≠ ∅
6 vx . . . . . . . . . . . 12 setvar 𝑥
76cv 1537 . . . . . . . . . . 11 class 𝑥
8 vz . . . . . . . . . . . 12 setvar 𝑧
98cv 1537 . . . . . . . . . . 11 class 𝑧
10 vr . . . . . . . . . . . 12 setvar 𝑟
1110cv 1537 . . . . . . . . . . 11 class 𝑟
127, 9, 11wbr 5033 . . . . . . . . . 10 wff 𝑥𝑟𝑧
13 vy . . . . . . . . . . . 12 setvar 𝑦
1413cv 1537 . . . . . . . . . . 11 class 𝑦
1514, 9, 11wbr 5033 . . . . . . . . . 10 wff 𝑦𝑟𝑧
1612, 15wa 399 . . . . . . . . 9 wff (𝑥𝑟𝑧𝑦𝑟𝑧)
1716, 8, 3wrex 3110 . . . . . . . 8 wff 𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
1817, 13, 3wral 3109 . . . . . . 7 wff 𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
1918, 6, 3wral 3109 . . . . . 6 wff 𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧)
205, 19wa 399 . . . . 5 wff (𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
21 vf . . . . . . 7 setvar 𝑓
2221cv 1537 . . . . . 6 class 𝑓
23 cple 16567 . . . . . 6 class le
2422, 23cfv 6328 . . . . 5 class (le‘𝑓)
2520, 10, 24wsbc 3723 . . . 4 wff [(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
26 cbs 16478 . . . . 5 class Base
2722, 26cfv 6328 . . . 4 class (Base‘𝑓)
2825, 2, 27wsbc 3723 . . 3 wff [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))
29 cproset 17531 . . 3 class Proset
3028, 21, 29crab 3113 . 2 class {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
311, 30wceq 1538 1 wff Dirset = {𝑓 ∈ Proset ∣ [(Base‘𝑓) / 𝑏][(le‘𝑓) / 𝑟](𝑏 ≠ ∅ ∧ ∀𝑥𝑏𝑦𝑏𝑧𝑏 (𝑥𝑟𝑧𝑦𝑟𝑧))}
Colors of variables: wff setvar class
This definition is referenced by:  isdrs  17539
  Copyright terms: Public domain W3C validator