Theorem foco

Description: Composition of onto functions. (Contributed by NM, 22-Mar-2006)

	Ref	Expression
Assertion	foco	|- ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C )

Proof

Step	Hyp	Ref	Expression
1		dffo2	|- ( F : B -onto-> C <-> ( F : B --> C /\ ran F = C ) )
2		dffo2	|- ( G : A -onto-> B <-> ( G : A --> B /\ ran G = B ) )
3		fco	|- ( ( F : B --> C /\ G : A --> B ) -> ( F o. G ) : A --> C )
4	3	ad2ant2r	|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ( F o. G ) : A --> C )
5		fdm	|- ( F : B --> C -> dom F = B )
6		eqtr3	|- ( ( dom F = B /\ ran G = B ) -> dom F = ran G )
7	5 6	sylan	|- ( ( F : B --> C /\ ran G = B ) -> dom F = ran G )
8		rncoeq	|- ( dom F = ran G -> ran ( F o. G ) = ran F )
9	8	eqeq1d	|- ( dom F = ran G -> ( ran ( F o. G ) = C <-> ran F = C ) )
10	9	biimpar	|- ( ( dom F = ran G /\ ran F = C ) -> ran ( F o. G ) = C )
11	7 10	sylan	|- ( ( ( F : B --> C /\ ran G = B ) /\ ran F = C ) -> ran ( F o. G ) = C )
12	11	an32s	|- ( ( ( F : B --> C /\ ran F = C ) /\ ran G = B ) -> ran ( F o. G ) = C )
13	12	adantrl	|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ran ( F o. G ) = C )
14	4 13	jca	|- ( ( ( F : B --> C /\ ran F = C ) /\ ( G : A --> B /\ ran G = B ) ) -> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) )
15	1 2 14	syl2anb	|- ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) )
16		dffo2	|- ( ( F o. G ) : A -onto-> C <-> ( ( F o. G ) : A --> C /\ ran ( F o. G ) = C ) )
17	15 16	sylibr	|- ( ( F : B -onto-> C /\ G : A -onto-> B ) -> ( F o. G ) : A -onto-> C )