Metamath Proof Explorer

Theorem finxpreclem3

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

Ref Expression
Hypothesis finxpreclem3.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 finxpreclem3 
|- ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> <. U. N , ( 1st ` X ) >. = ( F ` <. N , X >. ) )

Proof

Step Hyp Ref Expression
1 finxpreclem3.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 1 a1i 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> 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 >. ) ) ) )
3 eqeq1 
 |-  ( n = N -> ( n = 1o <-> N = 1o ) )
4 eleq1 
 |-  ( x = X -> ( x e. U <-> X e. U ) )
5 3 4 bi2anan9 
 |-  ( ( n = N /\ x = X ) -> ( ( n = 1o /\ x e. U ) <-> ( N = 1o /\ X e. U ) ) )
6 eleq1 
 |-  ( x = X -> ( x e. ( _V X. U ) <-> X e. ( _V X. U ) ) )
7 6 adantl 
 |-  ( ( n = N /\ x = X ) -> ( x e. ( _V X. U ) <-> X e. ( _V X. U ) ) )
8 unieq 
 |-  ( n = N -> U. n = U. N )
9 8 adantr 
 |-  ( ( n = N /\ x = X ) -> U. n = U. N )
10 fveq2 
 |-  ( x = X -> ( 1st ` x ) = ( 1st ` X ) )
11 10 adantl 
 |-  ( ( n = N /\ x = X ) -> ( 1st ` x ) = ( 1st ` X ) )
12 9 11 opeq12d 
 |-  ( ( n = N /\ x = X ) -> <. U. n , ( 1st ` x ) >. = <. U. N , ( 1st ` X ) >. )
13 opeq12 
 |-  ( ( n = N /\ x = X ) -> <. n , x >. = <. N , X >. )
14 7 12 13 ifbieq12d 
 |-  ( ( n = N /\ x = X ) -> if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = if ( X e. ( _V X. U ) , <. U. N , ( 1st ` X ) >. , <. N , X >. ) )
15 5 14 ifbieq2d 
 |-  ( ( n = N /\ x = X ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = if ( ( N = 1o /\ X e. U ) , (/) , if ( X e. ( _V X. U ) , <. U. N , ( 1st ` X ) >. , <. N , X >. ) ) )
16 sssucid 
 |-  1o C_ suc 1o
17 df-2o 
 |-  2o = suc 1o
18 16 17 sseqtrri 
 |-  1o C_ 2o
19 1on 
 |-  1o e. On
20 17 19 sucneqoni 
 |-  2o =/= 1o
21 20 necomi 
 |-  1o =/= 2o
22 df-pss 
 |-  ( 1o C. 2o <-> ( 1o C_ 2o /\ 1o =/= 2o ) )
23 18 21 22 mpbir2an 
 |-  1o C. 2o
24 ssnpss 
 |-  ( 2o C_ 1o -> -. 1o C. 2o )
25 23 24 mt2 
 |-  -. 2o C_ 1o
26 sseq2 
 |-  ( N = 1o -> ( 2o C_ N <-> 2o C_ 1o ) )
27 25 26 mtbiri 
 |-  ( N = 1o -> -. 2o C_ N )
28 27 con2i 
 |-  ( 2o C_ N -> -. N = 1o )
29 28 intnanrd 
 |-  ( 2o C_ N -> -. ( N = 1o /\ X e. U ) )
30 29 iffalsed 
 |-  ( 2o C_ 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 >. ) )
31 iftrue 
 |-  ( X e. ( _V X. U ) -> if ( X e. ( _V X. U ) , <. U. N , ( 1st ` X ) >. , <. N , X >. ) = <. U. N , ( 1st ` X ) >. )
32 30 31 sylan9eq 
 |-  ( ( 2o C_ N /\ X e. ( _V X. U ) ) -> if ( ( N = 1o /\ X e. U ) , (/) , if ( X e. ( _V X. U ) , <. U. N , ( 1st ` X ) >. , <. N , X >. ) ) = <. U. N , ( 1st ` X ) >. )
33 15 32 sylan9eqr 
 |-  ( ( ( 2o C_ N /\ X e. ( _V X. U ) ) /\ ( n = N /\ x = X ) ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = <. U. N , ( 1st ` X ) >. )
34 33 adantlll 
 |-  ( ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) /\ ( n = N /\ x = X ) ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = <. U. N , ( 1st ` X ) >. )
35 simpll 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> N e. _om )
36 elex 
 |-  ( X e. ( _V X. U ) -> X e. _V )
37 36 adantl 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> X e. _V )
38 opex 
 |-  <. U. N , ( 1st ` X ) >. e. _V
39 38 a1i 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> <. U. N , ( 1st ` X ) >. e. _V )
40 2 34 35 37 39 ovmpod 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> ( N F X ) = <. U. N , ( 1st ` X ) >. )
41 df-ov 
 |-  ( N F X ) = ( F ` <. N , X >. )
42 40 41 eqtr3di 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ X e. ( _V X. U ) ) -> <. U. N , ( 1st ` X ) >. = ( F ` <. N , X >. ) )