Metamath Proof Explorer

Definition df-drs

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 aleast 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)

Ref Expression
Assertion df-drs ⊢ Dirset = f ∈ Proset | [˙Base f / b]˙ [˙≤ f / r]˙ b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdrs class Dirset
1 vf setvar f
2 cproset class Proset
3 cbs class Base
4 1 cv setvar f
5 4 3 cfv class Base f
6 vb setvar b
7 cple class le
8 4 7 cfv class ≤ f
9 vr setvar r
10 6 cv setvar b
11 c0 class ∅
12 10 11 wne wff b ≠ ∅
13 vx setvar x
14 vy setvar y
15 vz setvar z
16 13 cv setvar x
17 9 cv setvar r
18 15 cv setvar z
19 16 18 17 wbr wff x r z
20 14 cv setvar y
21 20 18 17 wbr wff y r z
22 19 21 wa wff x r z ∧ y r z
23 22 15 10 wrex wff ∃ z ∈ b x r z ∧ y r z
24 23 14 10 wral wff ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
25 24 13 10 wral wff ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
26 12 25 wa wff b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
27 26 9 8 wsbc wff [˙≤ f / r]˙ b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
28 27 6 5 wsbc wff [˙Base f / b]˙ [˙≤ f / r]˙ b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
29 28 1 2 crab class f ∈ Proset | [˙Base f / b]˙ [˙≤ f / r]˙ b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z
30 0 29 wceq wff Dirset = f ∈ Proset | [˙Base f / b]˙ [˙≤ f / r]˙ b ≠ ∅ ∧ ∀ x ∈ b ∀ y ∈ b ∃ z ∈ b x r z ∧ y r z