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 )