Metamath Proof Explorer

Theorem csbfinxpg

Description: Distribute proper substitution through Cartesian exponentiation. (Contributed by ML, 25-Oct-2020)

Ref Expression
Assertion csbfinxpg 
|- ( A e. V -> [_ A / x ]_ ( U ^^ N ) = ( [_ A / x ]_ U ^^ [_ A / x ]_ N ) )

Proof

Step Hyp Ref Expression
1 df-finxp 
 |-  ( 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 ) ) }
2 1 csbeq2i 
 |-  [_ 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 
 |-  ( [. 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 
 |-  ( A e. V -> ( [. A / x ]. N e. _om <-> [_ A / x ]_ N e. _om ) )
5 sbceq2g 
 |-  ( 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 
 |-  [_ 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 
 |-  ( 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 csbmpo123 
 |-  ( 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 
 |-  ( A e. V -> [_ A / x ]_ _om = _om )
10 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ _V = _V )
11 csbif 
 |-  [_ 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 
 |-  ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) )
13 sbcg 
 |-  ( A e. V -> ( [. A / x ]. n = 1o <-> n = 1o ) )
14 sbcel12 
 |-  ( [. A / x ]. z e. U <-> [_ A / x ]_ z e. [_ A / x ]_ U )
15 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ z = z )
16 15 eleq1d 
 |-  ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ U <-> z e. [_ A / x ]_ U ) )
17 14 16 bitrid 
 |-  ( A e. V -> ( [. A / x ]. z e. U <-> z e. [_ A / x ]_ U ) )
18 13 17 anbi12d 
 |-  ( A e. V -> ( ( [. A / x ]. n = 1o /\ [. A / x ]. z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) )
19 12 18 bitrid 
 |-  ( A e. V -> ( [. A / x ]. ( n = 1o /\ z e. U ) <-> ( n = 1o /\ z e. [_ A / x ]_ U ) ) )
20 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ (/) = (/) )
21 csbif 
 |-  [_ 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 
 |-  ( [. A / x ]. z e. ( _V X. U ) <-> [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) )
23 csbxp 
 |-  [_ A / x ]_ ( _V X. U ) = ( [_ A / x ]_ _V X. [_ A / x ]_ U )
24 10 xpeq1d 
 |-  ( A e. V -> ( [_ A / x ]_ _V X. [_ A / x ]_ U ) = ( _V X. [_ A / x ]_ U ) )
25 23 24 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ ( _V X. U ) = ( _V X. [_ A / x ]_ U ) )
26 15 25 eleq12d 
 |-  ( A e. V -> ( [_ A / x ]_ z e. [_ A / x ]_ ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) )
27 22 26 bitrid 
 |-  ( A e. V -> ( [. A / x ]. z e. ( _V X. U ) <-> z e. ( _V X. [_ A / x ]_ U ) ) )
28 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ <. U. n , ( 1st ` z ) >. = <. U. n , ( 1st ` z ) >. )
29 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ <. n , z >. = <. n , z >. )
30 27 28 29 ifbieq12d 
 |-  ( 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 >. ) )
31 21 30 eqtrid 
 |-  ( 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 >. ) )
32 19 20 31 ifbieq12d 
 |-  ( 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 >. ) ) )
33 11 32 eqtrid 
 |-  ( 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 >. ) ) )
34 9 10 33 mpoeq123dv 
 |-  ( 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 >. ) ) ) )
35 8 34 eqtrd 
 |-  ( 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 csbopg 
 |-  ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , [_ A / x ]_ y >. )
37 csbconstg 
 |-  ( A e. V -> [_ A / x ]_ y = y )
38 37 opeq2d 
 |-  ( A e. V -> <. [_ A / x ]_ N , [_ A / x ]_ y >. = <. [_ A / x ]_ N , y >. )
39 36 38 eqtrd 
 |-  ( A e. V -> [_ A / x ]_ <. N , y >. = <. [_ A / x ]_ N , y >. )
40 rdgeq12 
 |-  ( ( [_ 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 >. ) )
41 35 39 40 syl2anc 
 |-  ( 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 >. ) )
42 7 41 eqtrd 
 |-  ( 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 >. ) )
43 42 fveq1d 
 |-  ( 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 ) )
44 6 43 eqtrid 
 |-  ( 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 ) )
45 44 eqeq2d 
 |-  ( 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 ) ) )
46 5 45 bitrd 
 |-  ( 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 ) ) )
47 4 46 anbi12d 
 |-  ( 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 ) ) ) )
48 3 47 bitrid 
 |-  ( 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 ) ) ) )
49 48 abbidv 
 |-  ( 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 
 |-  [_ 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 
 |-  ( [_ 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 ) ) }
52 49 50 51 3eqtr4g 
 |-  ( 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 ) )
53 2 52 eqtrid 
 |-  ( A e. V -> [_ A / x ]_ ( U ^^ N ) = ( [_ A / x ]_ U ^^ [_ A / x ]_ N ) )