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 o. G ) Fn B )

Proof

Step Hyp Ref Expression
1 df-f
 |-  ( G : B --> A <-> ( G Fn B /\ ran G C_ A ) )
2 fnco
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )
3 2 3expb
 |-  ( ( F Fn A /\ ( G Fn B /\ ran G C_ A ) ) -> ( F o. G ) Fn B )
4 1 3 sylan2b
 |-  ( ( F Fn A /\ G : B --> A ) -> ( F o. G ) Fn B )