Description: The composition of a one-to-one onto function and its converse equals the identity relation restricted to the function's range. (Contributed by NM, 13-Dec-2003) (Proof shortened by Stefan O'Rear, 12-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | f1ococnv2 | |- ( F : A -1-1-onto-> B -> ( F o. `' F ) = ( _I |` B ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1ofo | |- ( F : A -1-1-onto-> B -> F : A -onto-> B ) |
|
| 2 | fococnv2 | |- ( F : A -onto-> B -> ( F o. `' F ) = ( _I |` B ) ) |
|
| 3 | 1 2 | syl | |- ( F : A -1-1-onto-> B -> ( F o. `' F ) = ( _I |` B ) ) |