Metamath Proof Explorer

Theorem finxpreclem2

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

Ref Expression
Assertion finxpreclem2 
|- ( ( X e. _V /\ -. 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 nfv 
 |-  F/ x ( X e. _V /\ -. X e. U )
2 nfmpo2 
 |-  F/_ 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 >. ) ) )
3 nfcv 
 |-  F/_ x <. 1o , X >.
4 2 3 nffv 
 |-  F/_ 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 >. )
5 nfcv 
 |-  F/_ x (/)
6 4 5 nfne 
 |-  F/ 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 >. ) =/= (/)
7 1 6 nfim 
 |-  F/ x ( ( X e. _V /\ -. 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 >. ) =/= (/) )
8 nfv 
 |-  F/ n x = X
9 nfv 
 |-  F/ n ( X e. _V /\ -. X e. U )
10 nfmpo1 
 |-  F/_ n ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
11 nfcv 
 |-  F/_ n <. 1o , X >.
12 10 11 nffv 
 |-  F/_ n ( ( 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 >. )
13 nfcv 
 |-  F/_ n (/)
14 12 13 nfne 
 |-  F/ n ( ( 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 >. ) =/= (/)
15 9 14 nfim 
 |-  F/ n ( ( X e. _V /\ -. 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 >. ) =/= (/) )
16 8 15 nfim 
 |-  F/ n ( x = X -> ( ( X e. _V /\ -. 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 >. ) =/= (/) ) )
17 1onn 
 |-  1o e. _om
18 17 elexi 
 |-  1o e. _V
19 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 >. )
20 0ex 
 |-  (/) e. _V
21 opex 
 |-  <. U. n , ( 1st ` x ) >. e. _V
22 opex 
 |-  <. n , x >. e. _V
23 21 22 ifex 
 |-  if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) e. _V
24 20 23 ifex 
 |-  if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V
25 24 csbex 
 |-  [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V
26 25 csbex 
 |-  [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V
27 eqid 
 |-  ( 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 >. ) ) )
28 27 ovmpos 
 |-  ( ( 1o e. _om /\ X e. _V /\ [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) e. _V ) -> ( 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 ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
29 17 26 28 mp3an13 
 |-  ( X e. _V -> ( 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 ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
30 29 adantr 
 |-  ( ( X e. _V /\ ( -. X e. U /\ ( n = 1o /\ x = X ) ) ) -> ( 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 ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
31 csbeq1a 
 |-  ( x = X -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
32 csbeq1a 
 |-  ( n = 1o -> [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
33 31 32 sylan9eqr 
 |-  ( ( n = 1o /\ x = X ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
34 33 adantl 
 |-  ( ( -. 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 >. ) ) = [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) )
35 eleq1 
 |-  ( x = X -> ( x e. U <-> X e. U ) )
36 35 notbid 
 |-  ( x = X -> ( -. x e. U <-> -. X e. U ) )
37 36 biimprcd 
 |-  ( -. X e. U -> ( x = X -> -. x e. U ) )
38 pm3.14 
 |-  ( ( -. n = 1o \/ -. x e. U ) -> -. ( n = 1o /\ x e. U ) )
39 38 olcs 
 |-  ( -. x e. U -> -. ( n = 1o /\ x e. U ) )
40 37 39 syl6 
 |-  ( -. X e. U -> ( x = X -> -. ( n = 1o /\ x e. U ) ) )
41 iffalse 
 |-  ( -. ( n = 1o /\ x e. U ) -> 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 >. ) )
42 40 41 syl6 
 |-  ( -. X e. U -> ( x = X -> 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 >. ) ) )
43 42 imp 
 |-  ( ( -. X e. U /\ x = X ) -> 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 >. ) )
44 ifeqor 
 |-  ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. U. n , ( 1st ` x ) >. \/ if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. n , x >. )
45 vuniex 
 |-  U. n e. _V
46 fvex 
 |-  ( 1st ` x ) e. _V
47 45 46 opnzi 
 |-  <. U. n , ( 1st ` x ) >. =/= (/)
48 47 neii 
 |-  -. <. U. n , ( 1st ` x ) >. = (/)
49 eqeq1 
 |-  ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. U. n , ( 1st ` x ) >. -> ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) <-> <. U. n , ( 1st ` x ) >. = (/) ) )
50 48 49 mtbiri 
 |-  ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. U. n , ( 1st ` x ) >. -> -. if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) )
51 vex 
 |-  n e. _V
52 vex 
 |-  x e. _V
53 51 52 opnzi 
 |-  <. n , x >. =/= (/)
54 53 neii 
 |-  -. <. n , x >. = (/)
55 eqeq1 
 |-  ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. n , x >. -> ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) <-> <. n , x >. = (/) ) )
56 54 55 mtbiri 
 |-  ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. n , x >. -> -. if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) )
57 50 56 jaoi 
 |-  ( ( if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. U. n , ( 1st ` x ) >. \/ if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = <. n , x >. ) -> -. if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) )
58 44 57 mp1i 
 |-  ( ( -. X e. U /\ x = X ) -> -. if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) = (/) )
59 58 neqned 
 |-  ( ( -. X e. U /\ x = X ) -> if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) =/= (/) )
60 43 59 eqnetrd 
 |-  ( ( -. X e. U /\ x = X ) -> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) =/= (/) )
61 60 adantrl 
 |-  ( ( -. 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 >. ) ) =/= (/) )
62 34 61 eqnetrrd 
 |-  ( ( -. X e. U /\ ( n = 1o /\ x = X ) ) -> [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) =/= (/) )
63 62 adantl 
 |-  ( ( X e. _V /\ ( -. X e. U /\ ( n = 1o /\ x = X ) ) ) -> [_ 1o / n ]_ [_ X / x ]_ if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) =/= (/) )
64 30 63 eqnetrd 
 |-  ( ( X e. _V /\ ( -. X e. U /\ ( n = 1o /\ x = X ) ) ) -> ( 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 ) =/= (/) )
65 19 64 eqnetrrid 
 |-  ( ( X e. _V /\ ( -. X e. U /\ ( n = 1o /\ 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 >. ) =/= (/) )
66 65 ancom2s 
 |-  ( ( X e. _V /\ ( ( n = 1o /\ x = X ) /\ -. 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 >. ) =/= (/) )
67 66 an12s 
 |-  ( ( ( n = 1o /\ x = X ) /\ ( X e. _V /\ -. 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 >. ) =/= (/) )
68 67 exp31 
 |-  ( n = 1o -> ( x = X -> ( ( X e. _V /\ -. 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 >. ) =/= (/) ) ) )
69 16 18 68 vtoclef 
 |-  ( x = X -> ( ( X e. _V /\ -. 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 >. ) =/= (/) ) )
70 7 69 vtoclefex 
 |-  ( X e. _V -> ( ( X e. _V /\ -. 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 >. ) =/= (/) ) )
71 70 anabsi5 
 |-  ( ( X e. _V /\ -. 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 >. ) =/= (/) )
72 71 necomd 
 |-  ( ( X e. _V /\ -. 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 >. ) )
73 72 neneqd 
 |-  ( ( X e. _V /\ -. 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 >. ) )