Metamath Proof Explorer

Theorem fnfco

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

Ref Expression
Assertion fnfco ⊢ F Fn A ∧ G : B ⟶ A → F ∘ G Fn B

Proof

Step Hyp Ref Expression
1 df-f ⊢ G : B ⟶ A ↔ G Fn B ∧ ran ⁡ G ⊆ A
2 fnco ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn B
3 2 3expb ⊢ F Fn A ∧ G Fn B ∧ ran ⁡ G ⊆ A → F ∘ G Fn B
4 1 3 sylan2b ⊢ F Fn A ∧ G : B ⟶ A → F ∘ G Fn B