Theorem funresfunco

Description: Composition of two functions, generalization of funco . (Contributed by Alexander van der Vekens, 25-Jul-2017)

	Ref	Expression
Assertion	funresfunco	⊢ ( ( Fun ( 𝐹 ↾ ran 𝐺 ) ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		funco	⊢ ( ( Fun ( 𝐹 ↾ ran 𝐺 ) ∧ Fun 𝐺 ) → Fun ( ( 𝐹 ↾ ran 𝐺 ) ∘ 𝐺 ) )
2		ssid	⊢ ran 𝐺 ⊆ ran 𝐺
3		cores	⊢ ( ran 𝐺 ⊆ ran 𝐺 → ( ( 𝐹 ↾ ran 𝐺 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 ) )
4	2 3	ax-mp	⊢ ( ( 𝐹 ↾ ran 𝐺 ) ∘ 𝐺 ) = ( 𝐹 ∘ 𝐺 )
5	4	eqcomi	⊢ ( 𝐹 ∘ 𝐺 ) = ( ( 𝐹 ↾ ran 𝐺 ) ∘ 𝐺 )
6	5	funeqi	⊢ ( Fun ( 𝐹 ∘ 𝐺 ) ↔ Fun ( ( 𝐹 ↾ ran 𝐺 ) ∘ 𝐺 ) )
7	1 6	sylibr	⊢ ( ( Fun ( 𝐹 ↾ ran 𝐺 ) ∧ Fun 𝐺 ) → Fun ( 𝐹 ∘ 𝐺 ) )