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 ({I ↾}_{A}) = F$

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

Metamath Proof Explorer