This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )