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

Theorem ss2ixp 6845
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 3187 . . . . 5  |-  ( B 
C_  C  ->  (
( f `  x
)  e.  B  -> 
( f `  x
)  e.  C ) )
21ral2imi 2632 . . . 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 548 . . 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 3259 . 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 6834 . 2  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
6 df-ixp 6834 . 2  |-  X_ x  e.  A  C  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C
) }
74, 5, 63sstr4g 3232 1  |-  ( A. x  e.  A  B  C_  C  ->  X_ x  e.  A  B  C_  X_ x  e.  A  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1696   {cab 2282   A.wral 2556    C_ wss 3165    Fn wfn 5266   ` cfv 5271   X_cixp 6833
This theorem is referenced by:  ixpeq2  6846  boxcutc  6875  pwcfsdom  8221  prdsval  13371  prdshom  13382  sscpwex  13708  wunfunc  13789  wunnat  13846  dprdss  15280  psrbaglefi  16134  ptuni2  17287  ptcld  17323  ptclsg  17325  prdstopn  17338  xkopt  17365  tmdgsum2  17795  ressprdsds  17951  prdsbl  18053  dstr  25274  prdstotbnd  26621
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-in 3172  df-ss 3179  df-ixp 6834
  Copyright terms: Public domain W3C validator