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 18249
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 18247 . 2 class Dirset
2 vb . . . . . . . 8 setvar 𝑏
32cv 1541 . . . . . . 7 class 𝑏
4 c0 4323 . . . . . . 7 class βˆ…
53, 4wne 2941 . . . . . 6 wff 𝑏 β‰  βˆ…
6 vx . . . . . . . . . . . 12 setvar π‘₯
76cv 1541 . . . . . . . . . . 11 class π‘₯
8 vz . . . . . . . . . . . 12 setvar 𝑧
98cv 1541 . . . . . . . . . . 11 class 𝑧
10 vr . . . . . . . . . . . 12 setvar π‘Ÿ
1110cv 1541 . . . . . . . . . . 11 class π‘Ÿ
127, 9, 11wbr 5149 . . . . . . . . . 10 wff π‘₯π‘Ÿπ‘§
13 vy . . . . . . . . . . . 12 setvar 𝑦
1413cv 1541 . . . . . . . . . . 11 class 𝑦
1514, 9, 11wbr 5149 . . . . . . . . . 10 wff π‘¦π‘Ÿπ‘§
1612, 15wa 397 . . . . . . . . 9 wff (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§)
1716, 8, 3wrex 3071 . . . . . . . 8 wff βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§)
1817, 13, 3wral 3062 . . . . . . 7 wff βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§)
1918, 6, 3wral 3062 . . . . . 6 wff βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§)
205, 19wa 397 . . . . 5 wff (𝑏 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§))
21 vf . . . . . . 7 setvar 𝑓
2221cv 1541 . . . . . 6 class 𝑓
23 cple 17204 . . . . . 6 class le
2422, 23cfv 6544 . . . . 5 class (leβ€˜π‘“)
2520, 10, 24wsbc 3778 . . . 4 wff [(leβ€˜π‘“) / π‘Ÿ](𝑏 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§))
26 cbs 17144 . . . . 5 class Base
2722, 26cfv 6544 . . . 4 class (Baseβ€˜π‘“)
2825, 2, 27wsbc 3778 . . 3 wff [(Baseβ€˜π‘“) / 𝑏][(leβ€˜π‘“) / π‘Ÿ](𝑏 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§))
29 cproset 18246 . . 3 class Proset
3028, 21, 29crab 3433 . 2 class {𝑓 ∈ Proset ∣ [(Baseβ€˜π‘“) / 𝑏][(leβ€˜π‘“) / π‘Ÿ](𝑏 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§))}
311, 30wceq 1542 1 wff Dirset = {𝑓 ∈ Proset ∣ [(Baseβ€˜π‘“) / 𝑏][(leβ€˜π‘“) / π‘Ÿ](𝑏 β‰  βˆ… ∧ βˆ€π‘₯ ∈ 𝑏 βˆ€π‘¦ ∈ 𝑏 βˆƒπ‘§ ∈ 𝑏 (π‘₯π‘Ÿπ‘§ ∧ π‘¦π‘Ÿπ‘§))}
Colors of variables: wff setvar class
This definition is referenced by:  isdrs  18254
  Copyright terms: Public domain W3C validator