Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  csbfinxpg Structured version   Visualization version   Unicode version

Theorem csbfinxpg 31850
Description: Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020.)
Assertion
Ref Expression
csbfinxpg  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( U ^^ ^^ N )  =  ( [_ A  /  x ]_ U ^^ ^^ [_ A  /  x ]_ N ) )
Distinct variable group:    x, N
Allowed substitution hints:    A( x)    U( x)    V( x)

Proof of Theorem csbfinxpg
Dummy variables  n  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-finxp 31846 . . 3  |-  ( U ^^ ^^ N )  =  { y  |  ( N  e.  om  /\  (/)  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  N ) ) }
21csbeq2i 3786 . 2  |-  [_ A  /  x ]_ ( U ^^ ^^ N )  =  [_ A  /  x ]_ { y  |  ( N  e.  om  /\  (/)  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  N ) ) }
3 sbcan 3298 . . . . 5  |-  ( [. A  /  x ]. ( N  e.  om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) )  <->  ( [. A  /  x ]. N  e. 
om  /\  [. A  /  x ]. (/)  =  ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) ) )
4 sbcel1g 3780 . . . . . 6  |-  ( A  e.  V  ->  ( [. A  /  x ]. N  e.  om  <->  [_ A  /  x ]_ N  e.  om )
)
5 sbceq2g 3783 . . . . . . 7  |-  ( A  e.  V  ->  ( [. A  /  x ]. (/)  =  ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N )  <->  (/)  =  [_ A  /  x ]_ ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  N ) ) )
6 csbfv12 5914 . . . . . . . . 9  |-  [_ A  /  x ]_ ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N )  =  ( [_ A  /  x ]_ rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  [_ A  /  x ]_ N )
7 csbrdgg 31800 . . . . . . . . . . 11  |-  ( A  e.  V  ->  [_ A  /  x ]_ rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. )  =  rec ( [_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  [_ A  /  x ]_ <. N ,  y
>. ) )
8 csbmpt22g 31802 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) )  =  ( n  e. 
[_ A  /  x ]_ om ,  z  e. 
[_ A  /  x ]_ _V  |->  [_ A  /  x ]_ if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) )
9 csbconstg 3362 . . . . . . . . . . . . . 14  |-  ( A  e.  V  ->  [_ A  /  x ]_ om  =  om )
10 csbconstg 3362 . . . . . . . . . . . . . 14  |-  ( A  e.  V  ->  [_ A  /  x ]_ _V  =  _V )
11 csbif 3922 . . . . . . . . . . . . . . 15  |-  [_ A  /  x ]_ if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )  =  if ( [. A  /  x ]. ( n  =  1o  /\  z  e.  U ) ,  [_ A  /  x ]_ (/) ,  [_ A  /  x ]_ if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )
12 sbcan 3298 . . . . . . . . . . . . . . . . 17  |-  ( [. A  /  x ]. (
n  =  1o  /\  z  e.  U )  <->  (
[. A  /  x ]. n  =  1o  /\ 
[. A  /  x ]. z  e.  U
) )
13 sbcg 3321 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  V  ->  ( [. A  /  x ]. n  =  1o  <->  n  =  1o ) )
14 sbcel12 3776 . . . . . . . . . . . . . . . . . . 19  |-  ( [. A  /  x ]. z  e.  U  <->  [_ A  /  x ]_ z  e.  [_ A  /  x ]_ U )
15 csbconstg 3362 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  V  ->  [_ A  /  x ]_ z  =  z )
1615eleq1d 2533 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ z  e.  [_ A  /  x ]_ U  <->  z  e.  [_ A  /  x ]_ U ) )
1714, 16syl5bb 265 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  U  <->  z  e.  [_ A  /  x ]_ U ) )
1813, 17anbi12d 725 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  V  ->  (
( [. A  /  x ]. n  =  1o  /\ 
[. A  /  x ]. z  e.  U
)  <->  ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ) )
1912, 18syl5bb 265 . . . . . . . . . . . . . . . 16  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( n  =  1o 
/\  z  e.  U
)  <->  ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ) )
20 csbconstg 3362 . . . . . . . . . . . . . . . 16  |-  ( A  e.  V  ->  [_ A  /  x ]_ (/)  =  (/) )
21 csbif 3922 . . . . . . . . . . . . . . . . 17  |-  [_ A  /  x ]_ if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. )  =  if ( [. A  /  x ]. z  e.  ( _V  X.  U ) ,  [_ A  /  x ]_ <. U. n ,  ( 1st `  z )
>. ,  [_ A  /  x ]_ <. n ,  z
>. )
22 sbcel12 3776 . . . . . . . . . . . . . . . . . . 19  |-  ( [. A  /  x ]. z  e.  ( _V  X.  U
)  <->  [_ A  /  x ]_ z  e.  [_ A  /  x ]_ ( _V 
X.  U ) )
23 csbxp 4921 . . . . . . . . . . . . . . . . . . . . 21  |-  [_ A  /  x ]_ ( _V 
X.  U )  =  ( [_ A  /  x ]_ _V  X.  [_ A  /  x ]_ U
)
2410xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ _V  X.  [_ A  /  x ]_ U )  =  ( _V  X.  [_ A  /  x ]_ U ) )
2523, 24syl5eq 2517 . . . . . . . . . . . . . . . . . . . 20  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( _V 
X.  U )  =  ( _V  X.  [_ A  /  x ]_ U
) )
2615, 25eleq12d 2543 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ z  e.  [_ A  /  x ]_ ( _V 
X.  U )  <->  z  e.  ( _V  X.  [_ A  /  x ]_ U ) ) )
2722, 26syl5bb 265 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  V  ->  ( [. A  /  x ]. z  e.  ( _V  X.  U )  <->  z  e.  ( _V  X.  [_ A  /  x ]_ U ) ) )
28 csbconstg 3362 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. U. n ,  ( 1st `  z
) >.  =  <. U. n ,  ( 1st `  z
) >. )
29 csbconstg 3362 . . . . . . . . . . . . . . . . . 18  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. n ,  z >.  =  <. n ,  z >. )
3027, 28, 29ifbieq12d 3899 . . . . . . . . . . . . . . . . 17  |-  ( A  e.  V  ->  if ( [. A  /  x ]. z  e.  ( _V  X.  U ) , 
[_ A  /  x ]_ <. U. n ,  ( 1st `  z )
>. ,  [_ A  /  x ]_ <. n ,  z
>. )  =  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )
3121, 30syl5eq 2517 . . . . . . . . . . . . . . . 16  |-  ( A  e.  V  ->  [_ A  /  x ]_ if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. )  =  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )
3219, 20, 31ifbieq12d 3899 . . . . . . . . . . . . . . 15  |-  ( A  e.  V  ->  if ( [. A  /  x ]. ( n  =  1o 
/\  z  e.  U
) ,  [_ A  /  x ]_ (/) ,  [_ A  /  x ]_ if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )  =  if ( ( n  =  1o  /\  z  e.  [_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) )
3311, 32syl5eq 2517 . . . . . . . . . . . . . 14  |-  ( A  e.  V  ->  [_ A  /  x ]_ if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) )  =  if ( ( n  =  1o  /\  z  e.  [_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) )
349, 10, 33mpt2eq123dv 6372 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  (
n  e.  [_ A  /  x ]_ om , 
z  e.  [_ A  /  x ]_ _V  |->  [_ A  /  x ]_ if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) )  =  ( n  e.  om , 
z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) )
358, 34eqtrd 2505 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) )  =  ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  [_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z ) >. ,  <. n ,  z >. )
) ) )
36 csbopg2 31795 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. N , 
y >.  =  <. [_ A  /  x ]_ N ,  [_ A  /  x ]_ y >. )
37 csbconstg 3362 . . . . . . . . . . . . . 14  |-  ( A  e.  V  ->  [_ A  /  x ]_ y  =  y )
3837opeq2d 4165 . . . . . . . . . . . . 13  |-  ( A  e.  V  ->  <. [_ A  /  x ]_ N ,  [_ A  /  x ]_ y >.  =  <. [_ A  /  x ]_ N ,  y >. )
3936, 38eqtrd 2505 . . . . . . . . . . . 12  |-  ( A  e.  V  ->  [_ A  /  x ]_ <. N , 
y >.  =  <. [_ A  /  x ]_ N , 
y >. )
40 rdgeq12 7149 . . . . . . . . . . . 12  |-  ( (
[_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) )  =  ( n  e.  om , 
z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) )  /\  [_ A  /  x ]_ <. N , 
y >.  =  <. [_ A  /  x ]_ N , 
y >. )  ->  rec ( [_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  [_ A  /  x ]_ <. N ,  y >. )  =  rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) )
4135, 39, 40syl2anc 673 . . . . . . . . . . 11  |-  ( A  e.  V  ->  rec ( [_ A  /  x ]_ ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  [_ A  /  x ]_ <. N ,  y >. )  =  rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) )
427, 41eqtrd 2505 . . . . . . . . . 10  |-  ( A  e.  V  ->  [_ A  /  x ]_ rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. )  =  rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) )
4342fveq1d 5881 . . . . . . . . 9  |-  ( A  e.  V  ->  ( [_ A  /  x ]_ rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  [_ A  /  x ]_ N )  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. [_ A  /  x ]_ N ,  y >. ) `
 [_ A  /  x ]_ N ) )
446, 43syl5eq 2517 . . . . . . . 8  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N )  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. [_ A  /  x ]_ N ,  y >. ) `
 [_ A  /  x ]_ N ) )
4544eqeq2d 2481 . . . . . . 7  |-  ( A  e.  V  ->  ( (/)  =  [_ A  /  x ]_ ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  N )  <->  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) `  [_ A  /  x ]_ N ) ) )
465, 45bitrd 261 . . . . . 6  |-  ( A  e.  V  ->  ( [. A  /  x ]. (/)  =  ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N )  <->  (/)  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. [_ A  /  x ]_ N ,  y >. ) `
 [_ A  /  x ]_ N ) ) )
474, 46anbi12d 725 . . . . 5  |-  ( A  e.  V  ->  (
( [. A  /  x ]. N  e.  om  /\ 
[. A  /  x ]. (/)  =  ( rec ( ( n  e. 
om ,  z  e. 
_V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V 
X.  U ) , 
<. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) )  <->  ( [_ A  /  x ]_ N  e. 
om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) `  [_ A  /  x ]_ N ) ) ) )
483, 47syl5bb 265 . . . 4  |-  ( A  e.  V  ->  ( [. A  /  x ]. ( N  e.  om  /\  (/)  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e.  U ) ,  (/) ,  if ( z  e.  ( _V  X.  U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. N ,  y >. ) `  N ) )  <->  ( [_ A  /  x ]_ N  e.  om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) `  [_ A  /  x ]_ N ) ) ) )
4948abbidv 2589 . . 3  |-  ( A  e.  V  ->  { y  |  [. A  /  x ]. ( N  e. 
om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) ) }  =  {
y  |  ( [_ A  /  x ]_ N  e.  om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  [_ A  /  x ]_ U
) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. [_ A  /  x ]_ N ,  y >.
) `  [_ A  /  x ]_ N ) ) } )
50 csbab 3801 . . 3  |-  [_ A  /  x ]_ { y  |  ( N  e. 
om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) ) }  =  {
y  |  [. A  /  x ]. ( N  e.  om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) ) }
51 df-finxp 31846 . . 3  |-  ( [_ A  /  x ]_ U ^^ ^^ [_ A  /  x ]_ N )  =  { y  |  (
[_ A  /  x ]_ N  e.  om  /\  (/)  =  ( rec (
( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o  /\  z  e. 
[_ A  /  x ]_ U ) ,  (/) ,  if ( z  e.  ( _V  X.  [_ A  /  x ]_ U
) ,  <. U. n ,  ( 1st `  z
) >. ,  <. n ,  z >. )
) ) ,  <. [_ A  /  x ]_ N ,  y >. ) `
 [_ A  /  x ]_ N ) ) }
5249, 50, 513eqtr4g 2530 . 2  |-  ( A  e.  V  ->  [_ A  /  x ]_ { y  |  ( N  e. 
om  /\  (/)  =  ( rec ( ( n  e.  om ,  z  e.  _V  |->  if ( ( n  =  1o 
/\  z  e.  U
) ,  (/) ,  if ( z  e.  ( _V  X.  U ) ,  <. U. n ,  ( 1st `  z )
>. ,  <. n ,  z >. ) ) ) ,  <. N ,  y
>. ) `  N ) ) }  =  (
[_ A  /  x ]_ U ^^ ^^ [_ A  /  x ]_ N ) )
532, 52syl5eq 2517 1  |-  ( A  e.  V  ->  [_ A  /  x ]_ ( U ^^ ^^ N )  =  ( [_ A  /  x ]_ U ^^ ^^ [_ A  /  x ]_ N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    = wceq 1452    e. wcel 1904   {cab 2457   _Vcvv 3031   [.wsbc 3255   [_csb 3349   (/)c0 3722   ifcif 3872   <.cop 3965   U.cuni 4190    X. cxp 4837   ` cfv 5589    |-> cmpt2 6310   omcom 6711   1stc1st 6810   reccrdg 7145   1oc1o 7193   ^^
^^cfinxp 31845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-mpt 4456  df-xp 4845  df-cnv 4847  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-iota 5553  df-fv 5597  df-oprab 6312  df-mpt2 6313  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-finxp 31846
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator