Theorem xpss12 4731

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

Assertion

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

Proof of Theorem xpss12

Dummy variables x y are mutually distinct and distinct from all other variables.

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

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   C_ wss 3129   {copab 4061   X. cxp 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-in 3135  df-ss 3142  df-opab 4063  df-xp 4630

This theorem is referenced by:  xpss  4732  xpss1  4734  xpss2  4735  djussxp  4769  ssxpbm  5061  ssrnres  5068  cossxp  5148  cossxp2  5149  cocnvss  5151  relrelss  5152  fssxp  5380  oprabss  5956  pmss12g  6670  caserel  7081  casef  7082  dmaddpi  7319  dmmulpi  7320  rexpssxrxp  7996  ltrelxr  8012  dfz2  9319  phimullem  12215  txuni2  13538  txbas  13540  neitx  13550  txcnp  13553  cnmpt2res  13579  psmetres2  13615  xmetres2  13661  metres2  13663  xmetresbl  13722  xmettx  13792  qtopbasss  13803  tgqioo  13829  resubmet  13830  limccnp2lem  13927  limccnp2cntop  13928