Step |
Hyp |
Ref |
Expression |
1 |
|
dirref.1 |
|- X = dom R |
2 |
|
dirdm |
|- ( R e. DirRel -> dom R = U. U. R ) |
3 |
1 2
|
syl5eq |
|- ( 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 ) |