Theorem focofo

Description: Composition of onto functions. Generalisation of foco . (Contributed by AV, 29-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		fof	|- ( F : A -onto-> B -> F : A --> B )
2		fcof	|- ( ( F : A --> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )
3	1 2	sylan	|- ( ( F : A -onto-> B /\ Fun G ) -> ( F o. G ) : ( `' G " A ) --> B )
4	3	3adant3	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ( F o. G ) : ( `' G " A ) --> B )
5		rnco	|- ran ( F o. G ) = ran ( F |` ran G )
6	1	freld	|- ( F : A -onto-> B -> Rel F )
7	6	3ad2ant1	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> Rel F )
8		fdm	|- ( F : A --> B -> dom F = A )
9	8	eqcomd	|- ( F : A --> B -> A = dom F )
10	1 9	syl	|- ( F : A -onto-> B -> A = dom F )
11	10	sseq1d	|- ( F : A -onto-> B -> ( A C_ ran G <-> dom F C_ ran G ) )
12	11	biimpa	|- ( ( F : A -onto-> B /\ A C_ ran G ) -> dom F C_ ran G )
13		relssres	|- ( ( Rel F /\ dom F C_ ran G ) -> ( F |` ran G ) = F )
14	13	rneqd	|- ( ( Rel F /\ dom F C_ ran G ) -> ran ( F |` ran G ) = ran F )
15	7 12 14	3imp3i2an	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F |` ran G ) = ran F )
16		forn	|- ( F : A -onto-> B -> ran F = B )
17	16	3ad2ant1	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran F = B )
18	15 17	eqtrd	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F |` ran G ) = B )
19	5 18	syl5eq	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ran ( F o. G ) = B )
20		dffo2	|- ( ( F o. G ) : ( `' G " A ) -onto-> B <-> ( ( F o. G ) : ( `' G " A ) --> B /\ ran ( F o. G ) = B ) )
21	4 19 20	sylanbrc	|- ( ( F : A -onto-> B /\ Fun G /\ A C_ ran G ) -> ( F o. G ) : ( `' G " A ) -onto-> B )