Description: Show that a function is the inverse of a function if their compositions are the identity functions. (Contributed by Mario Carneiro, 21-Mar-2015) (Revised by AV, 15-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fcof1od.f | |- ( ph -> F : A --> B ) |
|
| fcof1od.g | |- ( ph -> G : B --> A ) |
||
| fcof1od.a | |- ( ph -> ( G o. F ) = ( _I |` A ) ) |
||
| fcof1od.b | |- ( ph -> ( F o. G ) = ( _I |` B ) ) |
||
| Assertion | 2fcoidinvd | |- ( ph -> `' F = G ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fcof1od.f | |- ( ph -> F : A --> B ) |
|
| 2 | fcof1od.g | |- ( ph -> G : B --> A ) |
|
| 3 | fcof1od.a | |- ( ph -> ( G o. F ) = ( _I |` A ) ) |
|
| 4 | fcof1od.b | |- ( ph -> ( F o. G ) = ( _I |` B ) ) |
|
| 5 | 1 2 3 4 | fcof1od | |- ( ph -> F : A -1-1-onto-> B ) |
| 6 | 5 2 4 | fcof1oinvd | |- ( ph -> `' F = G ) |