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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdrs	⊢ Dirset
1		vf	⊢ 𝑓
2		cproset	⊢ Proset
3		cbs	⊢ Base
4	1	cv	⊢ 𝑓
5	4 3	cfv	⊢ ( Base ‘ 𝑓 )
6		vb	⊢ 𝑏
7		cple	⊢ le
8	4 7	cfv	⊢ ( le ‘ 𝑓 )
9		vr	⊢ 𝑟
10	6	cv	⊢ 𝑏
11		c0	⊢ ∅
12	10 11	wne	⊢ 𝑏 ≠ ∅
13		vx	⊢ 𝑥
14		vy	⊢ 𝑦
15		vz	⊢ 𝑧
16	13	cv	⊢ 𝑥
17	9	cv	⊢ 𝑟
18	15	cv	⊢ 𝑧
19	16 18 17	wbr	⊢ 𝑥 𝑟 𝑧
20	14	cv	⊢ 𝑦
21	20 18 17	wbr	⊢ 𝑦 𝑟 𝑧
22	19 21	wa	⊢ ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 )
23	22 15 10	wrex	⊢ ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 )
24	23 14 10	wral	⊢ ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 )
25	24 13 10	wral	⊢ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 )
26	12 25	wa	⊢ ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) )
27	26 9 8	wsbc	⊢ [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) )
28	27 6 5	wsbc	⊢ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) )
29	28 1 2	crab	⊢ { 𝑓 ∈ Proset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) }
30	0 29	wceq	⊢ Dirset = { 𝑓 ∈ Proset ∣ [ ( Base ‘ 𝑓 ) / 𝑏 ] [ ( le ‘ 𝑓 ) / 𝑟 ] ( 𝑏 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑏 ∀ 𝑦 ∈ 𝑏 ∃ 𝑧 ∈ 𝑏 ( 𝑥 𝑟 𝑧 ∧ 𝑦 𝑟 𝑧 ) ) }