Metamath Proof Explorer

Theorem finxpeq2

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

Ref Expression
Assertion finxpeq2 
|- ( M = N -> ( U ^^ M ) = ( U ^^ N ) )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( M = N -> ( M e. _om <-> N e. _om ) )
2 opeq1 
 |-  ( M = N -> <. M , y >. = <. N , y >. )
3 rdgeq2 
 |-  ( <. M , y >. = <. N , y >. -> 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 >. ) ) ) , <. M , y >. ) = 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 >. ) )
4 2 3 syl 
 |-  ( M = N -> 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 >. ) ) ) , <. M , y >. ) = 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 >. ) )
5 id 
 |-  ( M = N -> M = N )
6 4 5 fveq12d 
 |-  ( M = N -> ( 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 >. ) ) ) , <. M , y >. ) ` M ) = ( 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 ) )
7 6 eqeq2d 
 |-  ( M = N -> ( (/) = ( 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 >. ) ) ) , <. M , y >. ) ` M ) <-> (/) = ( 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 ) ) )
8 1 7 anbi12d 
 |-  ( M = N -> ( ( M 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 >. ) ) ) , <. M , y >. ) ` M ) ) <-> ( 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 ) ) ) )
9 8 abbidv 
 |-  ( M = N -> { y | ( M 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 >. ) ) ) , <. M , y >. ) ` M ) ) } = { 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 ) ) } )
10 df-finxp 
 |-  ( U ^^ M ) = { y | ( M 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 >. ) ) ) , <. M , y >. ) ` M ) ) }
11 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 ) ) }
12 9 10 11 3eqtr4g 
 |-  ( M = N -> ( U ^^ M ) = ( U ^^ N ) )