Theorem dirge

Description: For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have aleast upper bound. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Hypothesis	dirge.1	⊢ 𝑋 = dom 𝑅
Assertion	dirge	⊢ ( ( 𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		dirge.1	⊢ 𝑋 = dom 𝑅
2		dirdm	⊢ ( 𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅 )
3	1 2	eqtrid	⊢ ( 𝑅 ∈ DirRel → 𝑋 = ∪ ∪ 𝑅 )
4	3	eleq2d	⊢ ( 𝑅 ∈ DirRel → ( 𝐴 ∈ 𝑋 ↔ 𝐴 ∈ ∪ ∪ 𝑅 ) )
5	3	eleq2d	⊢ ( 𝑅 ∈ DirRel → ( 𝐵 ∈ 𝑋 ↔ 𝐵 ∈ ∪ ∪ 𝑅 ) )
6	4 5	anbi12d	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ↔ ( 𝐴 ∈ ∪ ∪ 𝑅 ∧ 𝐵 ∈ ∪ ∪ 𝑅 ) ) )
7		eqid	⊢ ∪ ∪ 𝑅 = ∪ ∪ 𝑅
8	7	isdir	⊢ ( 𝑅 ∈ DirRel → ( 𝑅 ∈ DirRel ↔ ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) ) )
9	8	ibi	⊢ ( 𝑅 ∈ DirRel → ( ( Rel 𝑅 ∧ ( I ↾ ∪ ∪ 𝑅 ) ⊆ 𝑅 ) ∧ ( ( 𝑅 ∘ 𝑅 ) ⊆ 𝑅 ∧ ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
10	9	simprrd	⊢ ( 𝑅 ∈ DirRel → ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) )
11		codir	⊢ ( ( ∪ ∪ 𝑅 × ∪ ∪ 𝑅 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∀ 𝑦 ∈ ∪ ∪ 𝑅 ∀ 𝑧 ∈ ∪ ∪ 𝑅 ∃ 𝑥 ( 𝑦 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) )
12	10 11	sylib	⊢ ( 𝑅 ∈ DirRel → ∀ 𝑦 ∈ ∪ ∪ 𝑅 ∀ 𝑧 ∈ ∪ ∪ 𝑅 ∃ 𝑥 ( 𝑦 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) )
13		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 𝑅 𝑥 ↔ 𝐴 𝑅 𝑥 ) )
14	13	anbi1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝑦 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ↔ ( 𝐴 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ) )
15	14	exbidv	⊢ ( 𝑦 = 𝐴 → ( ∃ 𝑥 ( 𝑦 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ) )
16		breq1	⊢ ( 𝑧 = 𝐵 → ( 𝑧 𝑅 𝑥 ↔ 𝐵 𝑅 𝑥 ) )
17	16	anbi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
18	17	exbidv	⊢ ( 𝑧 = 𝐵 → ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
19	15 18	rspc2v	⊢ ( ( 𝐴 ∈ ∪ ∪ 𝑅 ∧ 𝐵 ∈ ∪ ∪ 𝑅 ) → ( ∀ 𝑦 ∈ ∪ ∪ 𝑅 ∀ 𝑧 ∈ ∪ ∪ 𝑅 ∃ 𝑥 ( 𝑦 𝑅 𝑥 ∧ 𝑧 𝑅 𝑥 ) → ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
20	12 19	syl5com	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 ∈ ∪ ∪ 𝑅 ∧ 𝐵 ∈ ∪ ∪ 𝑅 ) → ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
21	6 20	sylbid	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
22		reldir	⊢ ( 𝑅 ∈ DirRel → Rel 𝑅 )
23		relelrn	⊢ ( ( Rel 𝑅 ∧ 𝐴 𝑅 𝑥 ) → 𝑥 ∈ ran 𝑅 )
24	22 23	sylan	⊢ ( ( 𝑅 ∈ DirRel ∧ 𝐴 𝑅 𝑥 ) → 𝑥 ∈ ran 𝑅 )
25	24	ex	⊢ ( 𝑅 ∈ DirRel → ( 𝐴 𝑅 𝑥 → 𝑥 ∈ ran 𝑅 ) )
26		ssun2	⊢ ran 𝑅 ⊆ ( dom 𝑅 ∪ ran 𝑅 )
27		dmrnssfld	⊢ ( dom 𝑅 ∪ ran 𝑅 ) ⊆ ∪ ∪ 𝑅
28	26 27	sstri	⊢ ran 𝑅 ⊆ ∪ ∪ 𝑅
29	28 3	sseqtrrid	⊢ ( 𝑅 ∈ DirRel → ran 𝑅 ⊆ 𝑋 )
30	29	sseld	⊢ ( 𝑅 ∈ DirRel → ( 𝑥 ∈ ran 𝑅 → 𝑥 ∈ 𝑋 ) )
31	25 30	syld	⊢ ( 𝑅 ∈ DirRel → ( 𝐴 𝑅 𝑥 → 𝑥 ∈ 𝑋 ) )
32	31	adantrd	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) → 𝑥 ∈ 𝑋 ) )
33	32	ancrd	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) → ( 𝑥 ∈ 𝑋 ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) ) )
34	33	eximdv	⊢ ( 𝑅 ∈ DirRel → ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) → ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) ) )
35		df-rex	⊢ ( ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝑋 ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
36	34 35	imbitrrdi	⊢ ( 𝑅 ∈ DirRel → ( ∃ 𝑥 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
37	21 36	syld	⊢ ( 𝑅 ∈ DirRel → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) ) )
38	37	3impib	⊢ ( ( 𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ∃ 𝑥 ∈ 𝑋 ( 𝐴 𝑅 𝑥 ∧ 𝐵 𝑅 𝑥 ) )