Metamath Proof Explorer


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 syl6ibr ( 𝑅 ∈ DirRel → ( ∃ 𝑥 ( 𝐴 𝑅 𝑥𝐵 𝑅 𝑥 ) → ∃ 𝑥𝑋 ( 𝐴 𝑅 𝑥𝐵 𝑅 𝑥 ) ) )
37 21 36 syld ( 𝑅 ∈ DirRel → ( ( 𝐴𝑋𝐵𝑋 ) → ∃ 𝑥𝑋 ( 𝐴 𝑅 𝑥𝐵 𝑅 𝑥 ) ) )
38 37 3impib ( ( 𝑅 ∈ DirRel ∧ 𝐴𝑋𝐵𝑋 ) → ∃ 𝑥𝑋 ( 𝐴 𝑅 𝑥𝐵 𝑅 𝑥 ) )