Description: A relation composed zero times is the (restricted) identity. (Contributed by Drahflow, 12-Nov-2015) (Revised by RP, 30-May-2020) (Revised by AV, 12-Jul-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | relexp0d.1 | |- ( ph -> Rel R ) |
|
| relexp0d.2 | |- ( ph -> R e. V ) |
||
| Assertion | relexp0d | |- ( ph -> ( R ^r 0 ) = ( _I |` U. U. R ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | relexp0d.1 | |- ( ph -> Rel R ) |
|
| 2 | relexp0d.2 | |- ( ph -> R e. V ) |
|
| 3 | relexp0 | |- ( ( R e. V /\ Rel R ) -> ( R ^r 0 ) = ( _I |` U. U. R ) ) |
|
| 4 | 2 1 3 | syl2anc | |- ( ph -> ( R ^r 0 ) = ( _I |` U. U. R ) ) |