Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 8-May-2011) (Proof shortened by OpenAI, 3-Jul-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | relcoi1 | |- ( Rel R -> ( R o. ( _I |` U. U. R ) ) = R ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | coires1 | |- ( R o. ( _I |` U. U. R ) ) = ( R |` U. U. R ) |
|
| 2 | relresfld | |- ( Rel R -> ( R |` U. U. R ) = R ) |
|
| 3 | 1 2 | syl5eq | |- ( Rel R -> ( R o. ( _I |` U. U. R ) ) = R ) |