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 
|- X = dom R
Assertion dirge 
|- ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) )

Proof

Step Hyp Ref Expression
1 dirge.1 
 |-  X = dom R
2 dirdm 
 |-  ( R e. DirRel -> dom R = U. U. R )
3 1 2 eqtrid 
 |-  ( R e. DirRel -> X = U. U. R )
4 3 eleq2d 
 |-  ( R e. DirRel -> ( A e. X <-> A e. U. U. R ) )
5 3 eleq2d 
 |-  ( R e. DirRel -> ( B e. X <-> B e. U. U. R ) )
6 4 5 anbi12d 
 |-  ( R e. DirRel -> ( ( A e. X /\ B e. X ) <-> ( A e. U. U. R /\ B e. U. U. R ) ) )
7 eqid 
 |-  U. U. R = U. U. R
8 7 isdir 
 |-  ( R e. DirRel -> ( R e. DirRel <-> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) ) )
9 8 ibi 
 |-  ( R e. DirRel -> ( ( Rel R /\ ( _I |` U. U. R ) C_ R ) /\ ( ( R o. R ) C_ R /\ ( U. U. R X. U. U. R ) C_ ( `' R o. R ) ) ) )
10 9 simprrd 
 |-  ( R e. DirRel -> ( U. U. R X. U. U. R ) C_ ( `' R o. R ) )
11 codir 
 |-  ( ( U. U. R X. U. U. R ) C_ ( `' R o. R ) <-> A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) )
12 10 11 sylib 
 |-  ( R e. DirRel -> A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) )
13 breq1 
 |-  ( y = A -> ( y R x <-> A R x ) )
14 13 anbi1d 
 |-  ( y = A -> ( ( y R x /\ z R x ) <-> ( A R x /\ z R x ) ) )
15 14 exbidv 
 |-  ( y = A -> ( E. x ( y R x /\ z R x ) <-> E. x ( A R x /\ z R x ) ) )
16 breq1 
 |-  ( z = B -> ( z R x <-> B R x ) )
17 16 anbi2d 
 |-  ( z = B -> ( ( A R x /\ z R x ) <-> ( A R x /\ B R x ) ) )
18 17 exbidv 
 |-  ( z = B -> ( E. x ( A R x /\ z R x ) <-> E. x ( A R x /\ B R x ) ) )
19 15 18 rspc2v 
 |-  ( ( A e. U. U. R /\ B e. U. U. R ) -> ( A. y e. U. U. R A. z e. U. U. R E. x ( y R x /\ z R x ) -> E. x ( A R x /\ B R x ) ) )
20 12 19 syl5com 
 |-  ( R e. DirRel -> ( ( A e. U. U. R /\ B e. U. U. R ) -> E. x ( A R x /\ B R x ) ) )
21 6 20 sylbid 
 |-  ( R e. DirRel -> ( ( A e. X /\ B e. X ) -> E. x ( A R x /\ B R x ) ) )
22 reldir 
 |-  ( R e. DirRel -> Rel R )
23 relelrn 
 |-  ( ( Rel R /\ A R x ) -> x e. ran R )
24 22 23 sylan 
 |-  ( ( R e. DirRel /\ A R x ) -> x e. ran R )
25 24 ex 
 |-  ( R e. DirRel -> ( A R x -> x e. ran R ) )
26 ssun2 
 |-  ran R C_ ( dom R u. ran R )
27 dmrnssfld 
 |-  ( dom R u. ran R ) C_ U. U. R
28 26 27 sstri 
 |-  ran R C_ U. U. R
29 28 3 sseqtrrid 
 |-  ( R e. DirRel -> ran R C_ X )
30 29 sseld 
 |-  ( R e. DirRel -> ( x e. ran R -> x e. X ) )
31 25 30 syld 
 |-  ( R e. DirRel -> ( A R x -> x e. X ) )
32 31 adantrd 
 |-  ( R e. DirRel -> ( ( A R x /\ B R x ) -> x e. X ) )
33 32 ancrd 
 |-  ( R e. DirRel -> ( ( A R x /\ B R x ) -> ( x e. X /\ ( A R x /\ B R x ) ) ) )
34 33 eximdv 
 |-  ( R e. DirRel -> ( E. x ( A R x /\ B R x ) -> E. x ( x e. X /\ ( A R x /\ B R x ) ) ) )
35 df-rex 
 |-  ( E. x e. X ( A R x /\ B R x ) <-> E. x ( x e. X /\ ( A R x /\ B R x ) ) )
36 34 35 syl6ibr 
 |-  ( R e. DirRel -> ( E. x ( A R x /\ B R x ) -> E. x e. X ( A R x /\ B R x ) ) )
37 21 36 syld 
 |-  ( R e. DirRel -> ( ( A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) ) )
38 37 3impib 
 |-  ( ( R e. DirRel /\ A e. X /\ B e. X ) -> E. x e. X ( A R x /\ B R x ) )