Theorem fco3OLD

Description: Obsolete version of funcofd as 20-Sep-2024. (Contributed by Glauco Siliprandi, 26-Jun-2021) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		fco3OLD.1	|- ( ph -> Fun F )
2		fco3OLD.2	|- ( ph -> Fun G )
3		funco	|- ( ( Fun F /\ Fun G ) -> Fun ( F o. G ) )
4	1 2 3	syl2anc	|- ( ph -> Fun ( F o. G ) )
5		fdmrn	|- ( Fun ( F o. G ) <-> ( F o. G ) : dom ( F o. G ) --> ran ( F o. G ) )
6	4 5	sylib	|- ( ph -> ( F o. G ) : dom ( F o. G ) --> ran ( F o. G ) )
7		dmco	|- dom ( F o. G ) = ( `' G " dom F )
8	7	feq2i	|- ( ( F o. G ) : dom ( F o. G ) --> ran ( F o. G ) <-> ( F o. G ) : ( `' G " dom F ) --> ran ( F o. G ) )
9	6 8	sylib	|- ( ph -> ( F o. G ) : ( `' G " dom F ) --> ran ( F o. G ) )
10		rncoss	|- ran ( F o. G ) C_ ran F
11	10	a1i	|- ( ph -> ran ( F o. G ) C_ ran F )
12	9 11	fssd	|- ( ph -> ( F o. G ) : ( `' G " dom F ) --> ran F )