Metamath Proof Explorer

Theorem fcoi1

Description: Composition of a mapping and restricted identity. (Contributed by NM, 13-Dec-2003) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion fcoi1 
|- ( F : A --> B -> ( F o. ( _I |` A ) ) = F )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 df-fn 
 |-  ( F Fn A <-> ( Fun F /\ dom F = A ) )
3 eqimss 
 |-  ( dom F = A -> dom F C_ A )
4 cnvi 
 |-  `' _I = _I
5 4 reseq1i 
 |-  ( `' _I |` A ) = ( _I |` A )
6 5 cnveqi 
 |-  `' ( `' _I |` A ) = `' ( _I |` A )
7 cnvresid 
 |-  `' ( _I |` A ) = ( _I |` A )
8 6 7 eqtr2i 
 |-  ( _I |` A ) = `' ( `' _I |` A )
9 8 coeq2i 
 |-  ( F o. ( _I |` A ) ) = ( F o. `' ( `' _I |` A ) )
10 cores2 
 |-  ( dom F C_ A -> ( F o. `' ( `' _I |` A ) ) = ( F o. _I ) )
11 9 10 syl5eq 
 |-  ( dom F C_ A -> ( F o. ( _I |` A ) ) = ( F o. _I ) )
12 3 11 syl 
 |-  ( dom F = A -> ( F o. ( _I |` A ) ) = ( F o. _I ) )
13 funrel 
 |-  ( Fun F -> Rel F )
14 coi1 
 |-  ( Rel F -> ( F o. _I ) = F )
15 13 14 syl 
 |-  ( Fun F -> ( F o. _I ) = F )
16 12 15 sylan9eqr 
 |-  ( ( Fun F /\ dom F = A ) -> ( F o. ( _I |` A ) ) = F )
17 2 16 sylbi 
 |-  ( F Fn A -> ( F o. ( _I |` A ) ) = F )
18 1 17 syl 
 |-  ( F : A --> B -> ( F o. ( _I |` A ) ) = F )