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

Theorem ss2ixp 7494
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 3503 . . . . 5  |-  ( B 
C_  C  ->  (
( f `  x
)  e.  B  -> 
( f `  x
)  e.  C ) )
21ral2imi 2855 . . . 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 3578 . 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 7482 . 2  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
6 df-ixp 7482 . 2  |-  X_ x  e.  A  C  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C
) }
74, 5, 63sstr4g 3550 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 1767   {cab 2452   A.wral 2817    C_ wss 3481    Fn wfn 5589   ` cfv 5594   X_cixp 7481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2822  df-in 3488  df-ss 3495  df-ixp 7482
This theorem is referenced by:  ixpeq2  7495  boxcutc  7524  pwcfsdom  8970  prdsval  14727  prdshom  14739  sscpwex  15062  wunfunc  15143  wunnat  15200  dprdss  16948  psrbaglefi  17893  psrbaglefiOLD  17894  ptuni2  19945  ptcld  19982  ptclsg  19984  prdstopn  19997  xkopt  20024  tmdgsum2  20463  ressprdsds  20742  prdsbl  20862  prdstotbnd  30208
  Copyright terms: Public domain W3C validator