Metamath Proof Explorer

Theorem finxpeq1

Description: Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020)

Ref Expression
Assertion finxpeq1 
|- ( U = V -> ( U ^^ N ) = ( V ^^ N ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( U = V -> ( x e. U <-> x e. V ) )
2 1 anbi2d 
 |-  ( U = V -> ( ( n = 1o /\ x e. U ) <-> ( n = 1o /\ x e. V ) ) )
3 xpeq2 
 |-  ( U = V -> ( _V X. U ) = ( _V X. V ) )
4 3 eleq2d 
 |-  ( U = V -> ( x e. ( _V X. U ) <-> x e. ( _V X. V ) ) )
5 4 ifbid 
 |-  ( U = V -> if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) )
6 2 5 ifbieq2d 
 |-  ( U = V -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
7 6 mpoeq3dv 
 |-  ( U = V -> ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) )
8 rdgeq1 
 |-  ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) -> rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) = rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) )
9 7 8 syl 
 |-  ( U = V -> rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) = rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) )
10 9 fveq1d 
 |-  ( U = V -> ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) )
11 10 eqeq2d 
 |-  ( U = V -> ( (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) <-> (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) )
12 11 anbi2d 
 |-  ( U = V -> ( ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) <-> ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) ) )
13 12 abbidv 
 |-  ( U = V -> { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) } = { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) } )
14 df-finxp 
 |-  ( U ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) }
15 df-finxp 
 |-  ( V ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. V ) , (/) , if ( x e. ( _V X. V ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) }
16 13 14 15 3eqtr4g 
 |-  ( U = V -> ( U ^^ N ) = ( V ^^ N ) )