Metamath Proof Explorer

Theorem xpss12

Description: Subset theorem for Cartesian product. Generalization of Theorem 101 of Suppes p. 52. (Contributed by NM, 26-Aug-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion xpss12 
|- ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( A C_ B -> ( x e. A -> x e. B ) )
2 ssel 
 |-  ( C C_ D -> ( y e. C -> y e. D ) )
3 1 2 im2anan9 
 |-  ( ( A C_ B /\ C C_ D ) -> ( ( x e. A /\ y e. C ) -> ( x e. B /\ y e. D ) ) )
4 3 ssopab2dv 
 |-  ( ( A C_ B /\ C C_ D ) -> { <. x , y >. | ( x e. A /\ y e. C ) } C_ { <. x , y >. | ( x e. B /\ y e. D ) } )
5 df-xp 
 |-  ( A X. C ) = { <. x , y >. | ( x e. A /\ y e. C ) }
6 df-xp 
 |-  ( B X. D ) = { <. x , y >. | ( x e. B /\ y e. D ) }
7 4 5 6 3sstr4g 
 |-  ( ( A C_ B /\ C C_ D ) -> ( A X. C ) C_ ( B X. D ) )