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

Metamath Proof Explorer

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 )