Metamath Proof Explorer

Theorem finxpreclem1

Description: Lemma for ^^ recursion theorems. (Contributed by ML, 17-Oct-2020)

Ref Expression
Assertion finxpreclem1 
|- ( X e. U -> (/) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , X >. ) )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( X e. U -> ( 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. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) )
2 eleq1a 
 |-  ( X e. U -> ( x = X -> x e. U ) )
3 2 anim2d 
 |-  ( X e. U -> ( ( n = 1o /\ x = X ) -> ( n = 1o /\ x e. U ) ) )
4 iftrue 
 |-  ( ( n = 1o /\ x e. U ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = (/) )
5 3 4 syl6 
 |-  ( X e. U -> ( ( n = 1o /\ x = X ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = (/) ) )
6 5 imp 
 |-  ( ( X e. U /\ ( n = 1o /\ x = X ) ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = (/) )
7 1onn 
 |-  1o e. _om
8 7 a1i 
 |-  ( X e. U -> 1o e. _om )
9 elex 
 |-  ( X e. U -> X e. _V )
10 0ex 
 |-  (/) e. _V
11 10 a1i 
 |-  ( X e. U -> (/) e. _V )
12 1 6 8 9 11 ovmpod 
 |-  ( X e. U -> ( 1o ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) X ) = (/) )
13 df-ov 
 |-  ( 1o ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) X ) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , X >. )
14 12 13 eqtr3di 
 |-  ( X e. U -> (/) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , X >. ) )