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

Metamath Proof Explorer

Theorem xpssres

Description: Restriction of a constant function (or other Cartesian product). (Contributed by Stefan O'Rear, 24-Jan-2015)

Ref Expression
Assertion xpssres 
|- ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( ( A X. B ) |` C ) = ( ( A X. B ) i^i ( C X. _V ) )
2 inxp 
 |-  ( ( A X. B ) i^i ( C X. _V ) ) = ( ( A i^i C ) X. ( B i^i _V ) )
3 inv1 
 |-  ( B i^i _V ) = B
4 3 xpeq2i 
 |-  ( ( A i^i C ) X. ( B i^i _V ) ) = ( ( A i^i C ) X. B )
5 1 2 4 3eqtri 
 |-  ( ( A X. B ) |` C ) = ( ( A i^i C ) X. B )
6 sseqin2 
 |-  ( C C_ A <-> ( A i^i C ) = C )
7 6 biimpi 
 |-  ( C C_ A -> ( A i^i C ) = C )
8 7 xpeq1d 
 |-  ( C C_ A -> ( ( A i^i C ) X. B ) = ( C X. B ) )
9 5 8 eqtrid 
 |-  ( C C_ A -> ( ( A X. B ) |` C ) = ( C X. B ) )