Theorem cofunex2g

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

	Ref	Expression
Assertion	cofunex2g	|- ( ( A e. V /\ Fun `' B ) -> ( A o. B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		cnvexg	|- ( A e. V -> `' A e. _V )
2		cofunexg	|- ( ( Fun `' B /\ `' A e. _V ) -> ( `' B o. `' A ) e. _V )
3	1 2	sylan2	|- ( ( Fun `' B /\ A e. V ) -> ( `' B o. `' A ) e. _V )
4		cnvco	|- `' ( `' B o. `' A ) = ( `' `' A o. `' `' B )
5		cocnvcnv2	|- ( `' `' A o. `' `' B ) = ( `' `' A o. B )
6		cocnvcnv1	|- ( `' `' A o. B ) = ( A o. B )
7	4 5 6	3eqtrri	|- ( A o. B ) = `' ( `' B o. `' A )
8		cnvexg	|- ( ( `' B o. `' A ) e. _V -> `' ( `' B o. `' A ) e. _V )
9	7 8	eqeltrid	|- ( ( `' B o. `' A ) e. _V -> ( A o. B ) e. _V )
10	3 9	syl	|- ( ( Fun `' B /\ A e. V ) -> ( A o. B ) e. _V )
11	10	ancoms	|- ( ( A e. V /\ Fun `' B ) -> ( A o. B ) e. _V )