Theorem xpssres

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

	Ref	Expression
Assertion	xpssres	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( 𝐶 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-res	⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) )
2		inxp	⊢ ( ( 𝐴 × 𝐵 ) ∩ ( 𝐶 × V ) ) = ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) )
3		inv1	⊢ ( 𝐵 ∩ V ) = 𝐵
4	3	xpeq2i	⊢ ( ( 𝐴 ∩ 𝐶 ) × ( 𝐵 ∩ V ) ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
5	1 2 4	3eqtri	⊢ ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( ( 𝐴 ∩ 𝐶 ) × 𝐵 )
6		sseqin2	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐶 ) = 𝐶 )
7	6	biimpi	⊢ ( 𝐶 ⊆ 𝐴 → ( 𝐴 ∩ 𝐶 ) = 𝐶 )
8	7	xpeq1d	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 ∩ 𝐶 ) × 𝐵 ) = ( 𝐶 × 𝐵 ) )
9	5 8	eqtrid	⊢ ( 𝐶 ⊆ 𝐴 → ( ( 𝐴 × 𝐵 ) ↾ 𝐶 ) = ( 𝐶 × 𝐵 ) )