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

Theorem ss2ixp 7389
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 3461 . . . . 5  |-  ( B 
C_  C  ->  (
( f `  x
)  e.  B  -> 
( f `  x
)  e.  C ) )
21ral2imi 2814 . . . 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 3536 . 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 7377 . 2  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
6 df-ixp 7377 . 2  |-  X_ x  e.  A  C  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C
) }
74, 5, 63sstr4g 3508 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 1758   {cab 2439   A.wral 2799    C_ wss 3439    Fn wfn 5524   ` cfv 5529   X_cixp 7376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-in 3446  df-ss 3453  df-ixp 7377
This theorem is referenced by:  ixpeq2  7390  boxcutc  7419  pwcfsdom  8861  prdsval  14515  prdshom  14527  sscpwex  14850  wunfunc  14931  wunnat  14988  dprdss  16651  psrbaglefi  17567  psrbaglefiOLD  17568  ptuni2  19284  ptcld  19321  ptclsg  19323  prdstopn  19336  xkopt  19363  tmdgsum2  19802  ressprdsds  20081  prdsbl  20201  prdstotbnd  28861
  Copyright terms: Public domain W3C validator