Theorem funcofd

Description: Composition of two functions as a function with domain and codomain. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof shortened by AV, 20-Sep-2024)

	Ref	Expression
Hypotheses	funcofd.1	|- ( ph -> Fun F )
	funcofd.2	|- ( ph -> Fun G )
Assertion	funcofd	|- ( ph -> ( F o. G ) : ( `' G " dom F ) --> ran F )

Proof

Step	Hyp	Ref	Expression
1		funcofd.1	|- ( ph -> Fun F )
2		funcofd.2	|- ( ph -> Fun G )
3		fdmrn	|- ( Fun F <-> F : dom F --> ran F )
4	1 3	sylib	|- ( ph -> F : dom F --> ran F )
5		fcof	|- ( ( F : dom F --> ran F /\ Fun G ) -> ( F o. G ) : ( `' G " dom F ) --> ran F )
6	4 2 5	syl2anc	|- ( ph -> ( F o. G ) : ( `' G " dom F ) --> ran F )