Theorem fcoi2

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	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐹 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) )
2		cores	⊢ ( ran 𝐹 ⊆ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐹 ) = ( I ∘ 𝐹 ) )
3		fnrel	⊢ ( 𝐹 Fn 𝐴 → Rel 𝐹 )
4		coi2	⊢ ( Rel 𝐹 → ( I ∘ 𝐹 ) = 𝐹 )
5	3 4	syl	⊢ ( 𝐹 Fn 𝐴 → ( I ∘ 𝐹 ) = 𝐹 )
6	2 5	sylan9eqr	⊢ ( ( 𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵 ) → ( ( I ↾ 𝐵 ) ∘ 𝐹 ) = 𝐹 )
7	1 6	sylbi	⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝐹 ) = 𝐹 )