Metamath Proof Explorer

Theorem cossxp

Description: Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Assertion cossxp 
|- ( A o. B ) C_ ( dom B X. ran A )

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 rncoss 
 |-  ran ( A o. B ) C_ ran A
6 xpss12 
 |-  ( ( dom ( A o. B ) C_ dom B /\ ran ( A o. B ) C_ ran A ) -> ( dom ( A o. B ) X. ran ( A o. B ) ) C_ ( dom B X. ran A ) )
7 4 5 6 mp2an 
 |-  ( dom ( A o. B ) X. ran ( A o. B ) ) C_ ( dom B X. ran A )
8 3 7 sstri 
 |-  ( A o. B ) C_ ( dom B X. ran A )