Theorem fcof

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

	Ref	Expression
Assertion	fcof	|- ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )

Proof

Step	Hyp	Ref	Expression
1		df-f	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
2		fncofn	|- ( ( F Fn A /\ Fun G ) -> ( F o. G ) Fn ( `' G " A ) )
3	2	ex	|- ( F Fn A -> ( Fun G -> ( F o. G ) Fn ( `' G " A ) ) )
4	3	adantr	|- ( ( F Fn A /\ ran F C_ B ) -> ( Fun G -> ( F o. G ) Fn ( `' G " A ) ) )
5		rncoss	|- ran ( F o. G ) C_ ran F
6		sstr	|- ( ( ran ( F o. G ) C_ ran F /\ ran F C_ B ) -> ran ( F o. G ) C_ B )
7	5 6	mpan	|- ( ran F C_ B -> ran ( F o. G ) C_ B )
8	7	adantl	|- ( ( F Fn A /\ ran F C_ B ) -> ran ( F o. G ) C_ B )
9	4 8	jctird	|- ( ( F Fn A /\ ran F C_ B ) -> ( Fun G -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) ) )
10	9	imp	|- ( ( ( F Fn A /\ ran F C_ B ) /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
11	1 10	sylanb	|- ( ( F : A --> B /\ Fun G ) -> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
12		df-f	|- ( ( F o. G ) : ( `' G " A ) --> B <-> ( ( F o. G ) Fn ( `' G " A ) /\ ran ( F o. G ) C_ B ) )
13	11 12	sylibr	|- ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )