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

Theorem ss2ixp 7519
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 3435 . . . . 5  |-  ( B 
C_  C  ->  (
( f `  x
)  e.  B  -> 
( f `  x
)  e.  C ) )
21ral2imi 2791 . . . 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 563 . . 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 3511 . 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 7507 . 2  |-  X_ x  e.  A  B  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  B
) }
6 df-ixp 7507 . 2  |-  X_ x  e.  A  C  =  { f  |  ( f  Fn  { x  |  x  e.  A }  /\  A. x  e.  A  ( f `  x )  e.  C
) }
74, 5, 63sstr4g 3482 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 367    e. wcel 1842   {cab 2387   A.wral 2753    C_ wss 3413    Fn wfn 5563   ` cfv 5568   X_cixp 7506
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-in 3420  df-ss 3427  df-ixp 7507
This theorem is referenced by:  ixpeq2  7520  boxcutc  7549  pwcfsdom  8989  prdsval  15067  prdshom  15079  sscpwex  15426  wunfunc  15510  wunnat  15567  dprdss  17394  psrbaglefi  18341  psrbaglefiOLD  18342  ptuni2  20367  ptcld  20404  ptclsg  20406  prdstopn  20419  xkopt  20446  tmdgsum2  20885  ressprdsds  21164  prdsbl  21284  prdstotbnd  31552
  Copyright terms: Public domain W3C validator