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