Metamath Proof Explorer

Theorem dffinxpf

Description: This theorem is the same as Definition df-finxp , except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis dffinxpf.1 
|- F = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
Assertion dffinxpf 
|- ( U ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) }

Proof

Step Hyp Ref Expression
1 dffinxpf.1 
 |-  F = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
2 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 ) ) }
3 rdgeq1 
 |-  ( F = ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) -> rec ( F , <. 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 >. ) ) ) , <. N , y >. ) )
4 1 3 ax-mp 
 |-  rec ( F , <. 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 >. ) ) ) , <. N , y >. )
5 4 fveq1i 
 |-  ( rec ( F , <. N , y >. ) ` 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 >. ) ) ) , <. N , y >. ) ` N )
6 5 eqeq2i 
 |-  ( (/) = ( rec ( F , <. N , y >. ) ` 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 >. ) ) ) , <. N , y >. ) ` N ) )
7 6 anbi2i 
 |-  ( ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) <-> ( 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 ) ) )
8 7 abbii 
 |-  { y | ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` 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 ) ) }
9 2 8 eqtr4i 
 |-  ( U ^^ N ) = { y | ( N e. _om /\ (/) = ( rec ( F , <. N , y >. ) ` N ) ) }