Metamath Proof Explorer

Theorem dirref

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

Ref Expression
Hypothesis dirref.1 
|- X = dom R
Assertion dirref 
|- ( ( R e. DirRel /\ A e. X ) -> A R A )

Proof

Step Hyp Ref Expression
1 dirref.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 reseq2d 
 |-  ( R e. DirRel -> ( _I |` X ) = ( _I |` U. U. R ) )
5 eqid 
 |-  U. U. R = U. U. R
6 5 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 ) ) ) ) )
7 6 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 ) ) ) )
8 7 simplrd 
 |-  ( R e. DirRel -> ( _I |` U. U. R ) C_ R )
9 4 8 eqsstrd 
 |-  ( R e. DirRel -> ( _I |` X ) C_ R )
10 9 ssbrd 
 |-  ( R e. DirRel -> ( A ( _I |` X ) A -> A R A ) )
11 eqid 
 |-  A = A
12 resieq 
 |-  ( ( A e. X /\ A e. X ) -> ( A ( _I |` X ) A <-> A = A ) )
13 12 anidms 
 |-  ( A e. X -> ( A ( _I |` X ) A <-> A = A ) )
14 11 13 mpbiri 
 |-  ( A e. X -> A ( _I |` X ) A )
15 10 14 impel 
 |-  ( ( R e. DirRel /\ A e. X ) -> A R A )