MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ss2ixp Structured version   Unicode version

Theorem ss2ixp 7484
Description: Subclass theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006.) (Revised by Mario Carneiro, 12-Aug-2016.)
Assertion
Ref Expression
ss2ixp  |-  ( A. x  e.  A  B  C_  C  ->  X_ x  e.  A  B  C_  X_ x  e.  A  C )

Proof of Theorem ss2ixp
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 ssel 3483 . . . . 5  |-  ( B 
C_  C  ->  (
( f `  x
)  e.  B  -> 
( f `  x
)  e.  C ) )
21ral2imi 2831 . . . 4  |-  ( A. x  e.  A  B  C_  C  ->  ( A. x  e.  A  (
f `  x )  e.  B  ->  A. x  e.  A  ( f `  x )  e.  C
) )
32anim2d 565 . . 3  |-  ( A. x  e.  A  B  C_  C  ->  ( (
f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
)  ->  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C ) ) )
43ss2abdv 3558 . 2  |-  ( A. x  e.  A  B  C_  C  ->  { f  |  ( f  Fn 
{ x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B ) } 
C_  { f  |  ( f  Fn  {
x  |  x  e.  A }  /\  A. x  e.  A  (
f `  x )  e.  C ) } )
5 df-ixp 7472 . 2  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
6 df-ixp 7472 . 2  |-  X_ x  e.  A  C  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C
) }
74, 5, 63sstr4g 3530 1  |-  ( A. x  e.  A  B  C_  C  ->  X_ x  e.  A  B  C_  X_ x  e.  A  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1804   {cab 2428   A.wral 2793    C_ wss 3461    Fn wfn 5573   ` cfv 5578   X_cixp 7471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-in 3468  df-ss 3475  df-ixp 7472
This theorem is referenced by:  ixpeq2  7485  boxcutc  7514  pwcfsdom  8961  prdsval  14834  prdshom  14846  sscpwex  15166  wunfunc  15247  wunnat  15304  dprdss  17055  psrbaglefi  18002  psrbaglefiOLD  18003  ptuni2  20055  ptcld  20092  ptclsg  20094  prdstopn  20107  xkopt  20134  tmdgsum2  20573  ressprdsds  20852  prdsbl  20972  prdstotbnd  30266
  Copyright terms: Public domain W3C validator