Theorem cofunexg

Description: Existence of a composition when the first member is a function. (Contributed by NM, 8-Oct-2007)

	Ref	Expression
Assertion	cofunexg	|- ( ( Fun A /\ B e. C ) -> ( A o. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		relco	|- Rel ( A o. B )
2		relssdmrn	|- ( Rel ( A o. B ) -> ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) )
3	1 2	ax-mp	|- ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) )
4		dmcoss	|- dom ( A o. B ) C_ dom B
5		dmexg	|- ( B e. C -> dom B e. _V )
6		ssexg	|- ( ( dom ( A o. B ) C_ dom B /\ dom B e. _V ) -> dom ( A o. B ) e. _V )
7	4 5 6	sylancr	|- ( B e. C -> dom ( A o. B ) e. _V )
8	7	adantl	|- ( ( Fun A /\ B e. C ) -> dom ( A o. B ) e. _V )
9		rnco	|- ran ( A o. B ) = ran ( A |` ran B )
10		rnexg	|- ( B e. C -> ran B e. _V )
11		resfunexg	|- ( ( Fun A /\ ran B e. _V ) -> ( A |` ran B ) e. _V )
12	10 11	sylan2	|- ( ( Fun A /\ B e. C ) -> ( A |` ran B ) e. _V )
13		rnexg	|- ( ( A |` ran B ) e. _V -> ran ( A |` ran B ) e. _V )
14	12 13	syl	|- ( ( Fun A /\ B e. C ) -> ran ( A |` ran B ) e. _V )
15	9 14	eqeltrid	|- ( ( Fun A /\ B e. C ) -> ran ( A o. B ) e. _V )
16	8 15	xpexd	|- ( ( Fun A /\ B e. C ) -> ( dom ( A o. B ) X. ran ( A o. B ) ) e. _V )
17		ssexg	|- ( ( ( A o. B ) C_ ( dom ( A o. B ) X. ran ( A o. B ) ) /\ ( dom ( A o. B ) X. ran ( A o. B ) ) e. _V ) -> ( A o. B ) e. _V )
18	3 16 17	sylancr	|- ( ( Fun A /\ B e. C ) -> ( A o. B ) e. _V )