Theorem fnfco

Description: Composition of two functions. (Contributed by NM, 22-May-2006)

	Ref	Expression
Assertion	fnfco	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		df-f	⊢ ( 𝐺 : 𝐵 ⟶ 𝐴 ↔ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) )
2		fnco	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )
3	2	3expb	⊢ ( ( 𝐹 Fn 𝐴 ∧ ( 𝐺 Fn 𝐵 ∧ ran 𝐺 ⊆ 𝐴 ) ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )
4	1 3	sylan2b	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) → ( 𝐹 ∘ 𝐺 ) Fn 𝐵 )