Description: Composition of restricted identity and a mapping. (Contributed by NM, 13-Dec-2003) (Proof shortened by Andrew Salmon, 17-Sep-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fcoi2 | |- ( F : A --> B -> ( ( _I |` B ) o. F ) = F ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-f | |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) ) |
|
| 2 | cores | |- ( ran F C_ B -> ( ( _I |` B ) o. F ) = ( _I o. F ) ) |
|
| 3 | fnrel | |- ( F Fn A -> Rel F ) |
|
| 4 | coi2 | |- ( Rel F -> ( _I o. F ) = F ) |
|
| 5 | 3 4 | syl | |- ( F Fn A -> ( _I o. F ) = F ) |
| 6 | 2 5 | sylan9eqr | |- ( ( F Fn A /\ ran F C_ B ) -> ( ( _I |` B ) o. F ) = F ) |
| 7 | 1 6 | sylbi | |- ( F : A --> B -> ( ( _I |` B ) o. F ) = F ) |