This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnco

Description: Composition of two functions with domains as a function with domain. (Contributed by NM, 22-May-2006) (Proof shortened by AV, 20-Sep-2024)

Ref Expression
Assertion fnco 
|- ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( G Fn B -> Fun G )
2 fncofn 
 |-  ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )
3 1 2 sylan2 
 |-  ( ( F Fn A /\ G Fn B ) -> ( F o. G ) Fn ( `' G " A ) )
4 3 3adant3 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn ( `' G " A ) )
5 cnvimassrndm 
 |-  ( ran G C_ A -> ( `' G " A ) = dom G )
6 5 3ad2ant3 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( `' G " A ) = dom G )
7 fndm 
 |-  ( G Fn B -> dom G = B )
8 7 3ad2ant2 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> dom G = B )
9 6 8 eqtr2d 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> B = ( `' G " A ) )
10 9 fneq2d 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( ( F o. G ) Fn B <-> ( F o. G ) Fn ( `' G " A ) ) )
11 4 10 mpbird 
 |-  ( ( F Fn A /\ G Fn B /\ ran G C_ A ) -> ( F o. G ) Fn B )