Metamath Proof Explorer

Theorem reldir

Description: A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009) (Revised by Mario Carneiro, 22-Nov-2013)

Ref Expression
Assertion reldir 
|- ( R e. DirRel -> Rel R )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. U. R = U. U. R
2 1 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 ) ) ) ) )
3 2 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 ) ) ) )
4 3 simplld 
 |-  ( R e. DirRel -> Rel R )