ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpss12 Unicode version

Theorem xpss12 4650
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.
StepHypRef Expression
1 ssel 3092 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
2 ssel 3092 . . . 4  |-  ( C 
C_  D  ->  (
y  e.  C  -> 
y  e.  D ) )
31, 2im2anan9 588 . . 3  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( ( x  e.  A  /\  y  e.  C )  ->  (
x  e.  B  /\  y  e.  D )
) )
43ssopab2dv 4204 . 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 4549 . 2  |-  ( A  X.  C )  =  { <. x ,  y
>.  |  ( x  e.  A  /\  y  e.  C ) }
6 df-xp 4549 . 2  |-  ( B  X.  D )  =  { <. x ,  y
>.  |  ( x  e.  B  /\  y  e.  D ) }
74, 5, 63sstr4g 3141 1  |-  ( ( A  C_  B  /\  C  C_  D )  -> 
( A  X.  C
)  C_  ( B  X.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    e. wcel 1481    C_ wss 3072   {copab 3992    X. cxp 4541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-in 3078  df-ss 3085  df-opab 3994  df-xp 4549
This theorem is referenced by:  xpss  4651  xpss1  4653  xpss2  4654  djussxp  4688  ssxpbm  4978  ssrnres  4985  cossxp  5065  cossxp2  5066  cocnvss  5068  relrelss  5069  fssxp  5294  oprabss  5861  pmss12g  6573  caserel  6976  casef  6977  dmaddpi  7153  dmmulpi  7154  rexpssxrxp  7830  ltrelxr  7845  dfz2  9143  phimullem  11928  txuni2  12455  txbas  12457  neitx  12467  txcnp  12470  cnmpt2res  12496  psmetres2  12532  xmetres2  12578  metres2  12580  xmetresbl  12639  xmettx  12709  qtopbasss  12720  tgqioo  12746  resubmet  12747  limccnp2lem  12844  limccnp2cntop  12845
  Copyright terms: Public domain W3C validator