# 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}\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}$

### Proof

Step Hyp Ref Expression
1 ffn ${⊢}{F}:{A}⟶{B}\to {F}Fn{A}$
2 df-fn ${⊢}{F}Fn{A}↔\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}={A}\right)$
3 eqimss ${⊢}\mathrm{dom}{F}={A}\to \mathrm{dom}{F}\subseteq {A}$
4 cnvi ${⊢}{\mathrm{I}}^{-1}=\mathrm{I}$
5 4 reseq1i ${⊢}{{\mathrm{I}}^{-1}↾}_{{A}}={\mathrm{I}↾}_{{A}}$
6 5 cnveqi ${⊢}{\left({{\mathrm{I}}^{-1}↾}_{{A}}\right)}^{-1}={\left({\mathrm{I}↾}_{{A}}\right)}^{-1}$
7 cnvresid ${⊢}{\left({\mathrm{I}↾}_{{A}}\right)}^{-1}={\mathrm{I}↾}_{{A}}$
8 6 7 eqtr2i ${⊢}{\mathrm{I}↾}_{{A}}={\left({{\mathrm{I}}^{-1}↾}_{{A}}\right)}^{-1}$
9 8 coeq2i ${⊢}{F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}\circ {\left({{\mathrm{I}}^{-1}↾}_{{A}}\right)}^{-1}$
10 cores2 ${⊢}\mathrm{dom}{F}\subseteq {A}\to {F}\circ {\left({{\mathrm{I}}^{-1}↾}_{{A}}\right)}^{-1}={F}\circ \mathrm{I}$
11 9 10 syl5eq ${⊢}\mathrm{dom}{F}\subseteq {A}\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}\circ \mathrm{I}$
12 3 11 syl ${⊢}\mathrm{dom}{F}={A}\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}\circ \mathrm{I}$
13 funrel ${⊢}\mathrm{Fun}{F}\to \mathrm{Rel}{F}$
14 coi1 ${⊢}\mathrm{Rel}{F}\to {F}\circ \mathrm{I}={F}$
15 13 14 syl ${⊢}\mathrm{Fun}{F}\to {F}\circ \mathrm{I}={F}$
16 12 15 sylan9eqr ${⊢}\left(\mathrm{Fun}{F}\wedge \mathrm{dom}{F}={A}\right)\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}$
17 2 16 sylbi ${⊢}{F}Fn{A}\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}$
18 1 17 syl ${⊢}{F}:{A}⟶{B}\to {F}\circ \left({\mathrm{I}↾}_{{A}}\right)={F}$