Metamath Proof Explorer


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 𝐵 )