Theorem resres 5198

Description: The restriction of a restriction. (Contributed by NM, 27-Mar-2008.)

Assertion

Ref	Expression
resres	|- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Proof of Theorem resres

Step	Hyp	Ref	Expression
1		df-res 4925	. 2 |- ( ( A |` B ) |` C ) = ( ( A |` B ) i^i ( C X. _V ) )
2		df-res 4925	. . 3 |- ( A |` B ) = ( A i^i ( B X. _V ) )
3	2	ineq1i 3610	. 2 |- ( ( A |` B ) i^i ( C X. _V ) ) = ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) )
4		xpindir 5050	. . . 4 |- ( ( B i^i C ) X. _V ) = ( ( B X. _V ) i^i ( C X. _V ) )
5	4	ineq2i 3611	. . 3 |- ( A i^i ( ( B i^i C ) X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
6		df-res 4925	. . 3 |- ( A |` ( B i^i C ) ) = ( A i^i ( ( B i^i C ) X. _V ) )
7		inass 3622	. . 3 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A i^i ( ( B X. _V ) i^i ( C X. _V ) ) )
8	5, 6, 7	3eqtr4ri 2422	. 2 |- ( ( A i^i ( B X. _V ) ) i^i ( C X. _V ) ) = ( A |` ( B i^i C ) )
9	1, 3, 8	3eqtri 2415	1 |- ( ( A |` B ) |` C ) = ( A |` ( B i^i C ) )

Syntax hints:   = wceq 1399   _Vcvv 3034   i^i cin 3388   X. cxp 4911   |` cres 4915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-opab 4426  df-xp 4919  df-rel 4920  df-res 4925

This theorem is referenced by:  rescom  5210  resabs1  5214  resima2  5219  resmpt3  5236  resdisj  5346  rescnvcnv  5378  fresin  5662  resdif  5744  curry1  6791  curry2  6794  pmresg  7365  gruima  9091  rlimres  13383  lo1res  13384  rlimresb  13390  lo1eq  13393  rlimeq  13394  fsets  14662  setsid  14677  sscres  15229  gsumzres  17031  gsumzresOLD  17035  txkgen  20238  tsmsresOLD  20730  tsmsres  20731  ressxms  21113  ressms  21114  dvres  22400  dvres3a  22403  cpnres  22425  dvmptres3  22444  rlimcnp2  23413  df1stres  27669  df2ndres  27670  indf1ofs  28174  wfrlem4  29511  frrlem4  29555  fouriersw  32180  fouriercn  32181  dfrcl2  38211  relexpaddss  38223