Theorem fncofn

Description: Composition of a function with domain and a function as a function with domain. Generalization of fnco . (Contributed by AV, 17-Sep-2024)

	Ref	Expression
Assertion	fncofn	|- ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn A -> Fun F )
2		funco	|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
3	1 2	sylan	|- ( ( F Fn A /\ Fun G ) -> Fun ( F o. G ) )
4	3	funfnd	|- ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn dom ( F o. G ) )
5		fndm	|- ( F Fn A -> dom F = A )
6	5	adantr	|- ( ( F Fn A /\ Fun G ) -> dom F = A )
7	6	eqcomd	|- ( ( F Fn A /\ Fun G ) -> A = dom F )
8	7	imaeq2d	|- ( ( F Fn A /\ Fun G ) -> ( `' G " A ) = ( `' G " dom F ) )
9		dmco	|- dom ( F o. G ) = ( `' G " dom F )
10	8 9	eqtr4di	|- ( ( F Fn A /\ Fun G ) -> ( `' G " A ) = dom ( F o. G ) )
11	10	fneq2d	|- ( ( F Fn A /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) <-> ( F o. G ) Fn dom ( F o. G ) ) )
12	4 11	mpbird	|- ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )