Metamath Proof Explorer

Theorem finxpreclem5

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

Ref Expression
Hypothesis finxpreclem5.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 finxpreclem5 
|- ( ( n e. _om /\ 1o e. n ) -> ( -. x e. ( _V X. U ) -> ( F ` <. n , x >. ) = <. n , x >. ) )

Proof

Step Hyp Ref Expression
1 finxpreclem5.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-ov 
 |-  ( n F x ) = ( F ` <. n , x >. )
3 vex 
 |-  x e. _V
4 0ex 
 |-  (/) e. _V
5 opex 
 |-  <. U. n , ( 1st ` x ) >. e. _V
6 opex 
 |-  <. n , x >. e. _V
7 5 6 ifex 
 |-  if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) e. _V
8 4 7 ifex 
 |-  if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V
9 1 ovmpt4g 
 |-  ( ( n e. _om /\ x e. _V /\ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V ) -> ( n F x ) = if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
10 3 8 9 mp3an23 
 |-  ( n e. _om -> ( n F x ) = if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
11 10 ad2antrr 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( n F x ) = if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
12 1on 
 |-  1o e. On
13 12 onirri 
 |-  -. 1o e. 1o
14 eleq2 
 |-  ( n = 1o -> ( 1o e. n <-> 1o e. 1o ) )
15 13 14 mtbiri 
 |-  ( n = 1o -> -. 1o e. n )
16 15 con2i 
 |-  ( 1o e. n -> -. n = 1o )
17 16 intnanrd 
 |-  ( 1o e. n -> -. ( n = 1o /\ x e. U ) )
18 17 iffalsed 
 |-  ( 1o e. n -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) )
19 18 adantl 
 |-  ( ( n e. _om /\ 1o e. n ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) )
20 iffalse 
 |-  ( -. x e. ( _V X. U ) -> if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. n , x >. )
21 19 20 sylan9eq 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = <. n , x >. )
22 11 21 eqtrd 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( n F x ) = <. n , x >. )
23 2 22 eqtr3id 
 |-  ( ( ( n e. _om /\ 1o e. n ) /\ -. x e. ( _V X. U ) ) -> ( F ` <. n , x >. ) = <. n , x >. )
24 23 ex 
 |-  ( ( n e. _om /\ 1o e. n ) -> ( -. x e. ( _V X. U ) -> ( F ` <. n , x >. ) = <. n , x >. ) )