Metamath Proof Explorer

Theorem finxpreclem4

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

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

Proof

Step Hyp Ref Expression
1 finxpreclem4.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 2onn 
 |-  2o e. _om
3 nnon 
 |-  ( N e. _om -> N e. On )
4 2on 
 |-  2o e. On
5 oawordeu 
 |-  ( ( ( 2o e. On /\ N e. On ) /\ 2o C_ N ) -> E! o e. On ( 2o +o o ) = N )
6 4 5 mpanl1 
 |-  ( ( N e. On /\ 2o C_ N ) -> E! o e. On ( 2o +o o ) = N )
7 riotasbc 
 |-  ( E! o e. On ( 2o +o o ) = N -> [. ( iota_ o e. On ( 2o +o o ) = N ) / o ]. ( 2o +o o ) = N )
8 6 7 syl 
 |-  ( ( N e. On /\ 2o C_ N ) -> [. ( iota_ o e. On ( 2o +o o ) = N ) / o ]. ( 2o +o o ) = N )
9 riotaex 
 |-  ( iota_ o e. On ( 2o +o o ) = N ) e. _V
10 sbceq1g 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. _V -> ( [. ( iota_ o e. On ( 2o +o o ) = N ) / o ]. ( 2o +o o ) = N <-> [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = N ) )
11 9 10 ax-mp 
 |-  ( [. ( iota_ o e. On ( 2o +o o ) = N ) / o ]. ( 2o +o o ) = N <-> [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = N )
12 csbov2g 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. _V -> [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = ( 2o +o [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ o ) )
13 9 12 ax-mp 
 |-  [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = ( 2o +o [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ o )
14 9 csbvargi 
 |-  [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ o = ( iota_ o e. On ( 2o +o o ) = N )
15 14 oveq2i 
 |-  ( 2o +o [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ o ) = ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) )
16 13 15 eqtri 
 |-  [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) )
17 16 eqeq1i 
 |-  ( [_ ( iota_ o e. On ( 2o +o o ) = N ) / o ]_ ( 2o +o o ) = N <-> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = N )
18 11 17 bitri 
 |-  ( [. ( iota_ o e. On ( 2o +o o ) = N ) / o ]. ( 2o +o o ) = N <-> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = N )
19 8 18 sylib 
 |-  ( ( N e. On /\ 2o C_ N ) -> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = N )
20 3 19 sylan 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = N )
21 simpl 
 |-  ( ( N e. _om /\ 2o C_ N ) -> N e. _om )
22 20 21 eqeltrd 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om )
23 riotacl 
 |-  ( E! o e. On ( 2o +o o ) = N -> ( iota_ o e. On ( 2o +o o ) = N ) e. On )
24 riotaund 
 |-  ( -. E! o e. On ( 2o +o o ) = N -> ( iota_ o e. On ( 2o +o o ) = N ) = (/) )
25 0elon 
 |-  (/) e. On
26 24 25 eqeltrdi 
 |-  ( -. E! o e. On ( 2o +o o ) = N -> ( iota_ o e. On ( 2o +o o ) = N ) e. On )
27 23 26 pm2.61i 
 |-  ( iota_ o e. On ( 2o +o o ) = N ) e. On
28 nnarcl 
 |-  ( ( 2o e. On /\ ( iota_ o e. On ( 2o +o o ) = N ) e. On ) -> ( ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om <-> ( 2o e. _om /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) ) )
29 4 28 mpan 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. On -> ( ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om <-> ( 2o e. _om /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) ) )
30 2 biantrur 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. _om <-> ( 2o e. _om /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) )
31 29 30 bitr4di 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. On -> ( ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om <-> ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) )
32 27 31 ax-mp 
 |-  ( ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om <-> ( iota_ o e. On ( 2o +o o ) = N ) e. _om )
33 22 32 sylib 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( iota_ o e. On ( 2o +o o ) = N ) e. _om )
34 nnacom 
 |-  ( ( 2o e. _om /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) -> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = ( ( iota_ o e. On ( 2o +o o ) = N ) +o 2o ) )
35 2 33 34 sylancr 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) = ( ( iota_ o e. On ( 2o +o o ) = N ) +o 2o ) )
36 df-2o 
 |-  2o = suc 1o
37 36 oveq2i 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) +o 2o ) = ( ( iota_ o e. On ( 2o +o o ) = N ) +o suc 1o )
38 1onn 
 |-  1o e. _om
39 nnasuc 
 |-  ( ( ( iota_ o e. On ( 2o +o o ) = N ) e. _om /\ 1o e. _om ) -> ( ( iota_ o e. On ( 2o +o o ) = N ) +o suc 1o ) = suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) )
40 33 38 39 sylancl 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( ( iota_ o e. On ( 2o +o o ) = N ) +o suc 1o ) = suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) )
41 37 40 syl5eq 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( ( iota_ o e. On ( 2o +o o ) = N ) +o 2o ) = suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) )
42 35 20 41 3eqtr3d 
 |-  ( ( N e. _om /\ 2o C_ N ) -> N = suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) )
43 3 adantr 
 |-  ( ( N e. _om /\ 2o C_ N ) -> N e. On )
44 sucidg 
 |-  ( 1o e. _om -> 1o e. suc 1o )
45 38 44 ax-mp 
 |-  1o e. suc 1o
46 45 36 eleqtrri 
 |-  1o e. 2o
47 ssel 
 |-  ( 2o C_ N -> ( 1o e. 2o -> 1o e. N ) )
48 46 47 mpi 
 |-  ( 2o C_ N -> 1o e. N )
49 48 ne0d 
 |-  ( 2o C_ N -> N =/= (/) )
50 49 adantl 
 |-  ( ( N e. _om /\ 2o C_ N ) -> N =/= (/) )
51 nnlim 
 |-  ( N e. _om -> -. Lim N )
52 51 adantr 
 |-  ( ( N e. _om /\ 2o C_ N ) -> -. Lim N )
53 onsucuni3 
 |-  ( ( N e. On /\ N =/= (/) /\ -. Lim N ) -> N = suc U. N )
54 43 50 52 53 syl3anc 
 |-  ( ( N e. _om /\ 2o C_ N ) -> N = suc U. N )
55 nnacom 
 |-  ( ( ( iota_ o e. On ( 2o +o o ) = N ) e. _om /\ 1o e. _om ) -> ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
56 33 38 55 sylancl 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
57 suceq 
 |-  ( ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) -> suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) = suc ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
58 56 57 syl 
 |-  ( ( N e. _om /\ 2o C_ N ) -> suc ( ( iota_ o e. On ( 2o +o o ) = N ) +o 1o ) = suc ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
59 42 54 58 3eqtr3d 
 |-  ( ( N e. _om /\ 2o C_ N ) -> suc U. N = suc ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
60 ordom 
 |-  Ord _om
61 ordelss 
 |-  ( ( Ord _om /\ N e. _om ) -> N C_ _om )
62 60 61 mpan 
 |-  ( N e. _om -> N C_ _om )
63 nnfi 
 |-  ( N e. _om -> N e. Fin )
64 nnunifi 
 |-  ( ( N C_ _om /\ N e. Fin ) -> U. N e. _om )
65 62 63 64 syl2anc 
 |-  ( N e. _om -> U. N e. _om )
66 65 adantr 
 |-  ( ( N e. _om /\ 2o C_ N ) -> U. N e. _om )
67 nnacl 
 |-  ( ( 1o e. _om /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) -> ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om )
68 38 33 67 sylancr 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om )
69 peano4 
 |-  ( ( U. N e. _om /\ ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) e. _om ) -> ( suc U. N = suc ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) <-> U. N = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) )
70 66 68 69 syl2anc 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( suc U. N = suc ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) <-> U. N = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) )
71 59 70 mpbid 
 |-  ( ( N e. _om /\ 2o C_ N ) -> U. N = ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) )
72 71 fveq2d 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` U. N ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) )
73 72 adantr 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` U. N ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) )
74 33 adantr 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( iota_ o e. On ( 2o +o o ) = N ) e. _om )
75 df-1o 
 |-  1o = suc (/)
76 75 fveq2i 
 |-  ( rec ( F , <. N , y >. ) ` 1o ) = ( rec ( F , <. N , y >. ) ` suc (/) )
77 rdgsuc 
 |-  ( (/) e. On -> ( rec ( F , <. N , y >. ) ` suc (/) ) = ( F ` ( rec ( F , <. N , y >. ) ` (/) ) ) )
78 25 77 ax-mp 
 |-  ( rec ( F , <. N , y >. ) ` suc (/) ) = ( F ` ( rec ( F , <. N , y >. ) ` (/) ) )
79 opex 
 |-  <. N , y >. e. _V
80 79 rdg0 
 |-  ( rec ( F , <. N , y >. ) ` (/) ) = <. N , y >.
81 80 fveq2i 
 |-  ( F ` ( rec ( F , <. N , y >. ) ` (/) ) ) = ( F ` <. N , y >. )
82 76 78 81 3eqtri 
 |-  ( rec ( F , <. N , y >. ) ` 1o ) = ( F ` <. N , y >. )
83 1 finxpreclem3 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> <. U. N , ( 1st ` y ) >. = ( F ` <. N , y >. ) )
84 82 83 eqtr4id 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. N , y >. ) ` 1o ) = <. U. N , ( 1st ` y ) >. )
85 84 fveq2d 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( F ` ( rec ( F , <. N , y >. ) ` 1o ) ) = ( F ` <. U. N , ( 1st ` y ) >. ) )
86 2on0 
 |-  2o =/= (/)
87 nnlim 
 |-  ( 2o e. _om -> -. Lim 2o )
88 2 87 ax-mp 
 |-  -. Lim 2o
89 rdgsucuni 
 |-  ( ( 2o e. On /\ 2o =/= (/) /\ -. Lim 2o ) -> ( rec ( F , <. N , y >. ) ` 2o ) = ( F ` ( rec ( F , <. N , y >. ) ` U. 2o ) ) )
90 4 86 88 89 mp3an 
 |-  ( rec ( F , <. N , y >. ) ` 2o ) = ( F ` ( rec ( F , <. N , y >. ) ` U. 2o ) )
91 1oequni2o 
 |-  1o = U. 2o
92 91 fveq2i 
 |-  ( rec ( F , <. N , y >. ) ` 1o ) = ( rec ( F , <. N , y >. ) ` U. 2o )
93 92 fveq2i 
 |-  ( F ` ( rec ( F , <. N , y >. ) ` 1o ) ) = ( F ` ( rec ( F , <. N , y >. ) ` U. 2o ) )
94 90 93 eqtr4i 
 |-  ( rec ( F , <. N , y >. ) ` 2o ) = ( F ` ( rec ( F , <. N , y >. ) ` 1o ) )
95 75 fveq2i 
 |-  ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` 1o ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` suc (/) )
96 rdgsuc 
 |-  ( (/) e. On -> ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` suc (/) ) = ( F ` ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` (/) ) ) )
97 25 96 ax-mp 
 |-  ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` suc (/) ) = ( F ` ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` (/) ) )
98 opex 
 |-  <. U. N , ( 1st ` y ) >. e. _V
99 98 rdg0 
 |-  ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` (/) ) = <. U. N , ( 1st ` y ) >.
100 99 fveq2i 
 |-  ( F ` ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` (/) ) ) = ( F ` <. U. N , ( 1st ` y ) >. )
101 95 97 100 3eqtri 
 |-  ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` 1o ) = ( F ` <. U. N , ( 1st ` y ) >. )
102 85 94 101 3eqtr4g 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. N , y >. ) ` 2o ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` 1o ) )
103 1on 
 |-  1o e. On
104 rdgeqoa 
 |-  ( ( 2o e. On /\ 1o e. On /\ ( iota_ o e. On ( 2o +o o ) = N ) e. _om ) -> ( ( rec ( F , <. N , y >. ) ` 2o ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` 1o ) -> ( rec ( F , <. N , y >. ) ` ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) ) )
105 4 103 104 mp3an12 
 |-  ( ( iota_ o e. On ( 2o +o o ) = N ) e. _om -> ( ( rec ( F , <. N , y >. ) ` 2o ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` 1o ) -> ( rec ( F , <. N , y >. ) ` ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) ) )
106 74 102 105 sylc 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. N , y >. ) ` ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` ( 1o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) )
107 20 fveq2d 
 |-  ( ( N e. _om /\ 2o C_ N ) -> ( rec ( F , <. N , y >. ) ` ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) = ( rec ( F , <. N , y >. ) ` N ) )
108 107 adantr 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. N , y >. ) ` ( 2o +o ( iota_ o e. On ( 2o +o o ) = N ) ) ) = ( rec ( F , <. N , y >. ) ` N ) )
109 73 106 108 3eqtr2rd 
 |-  ( ( ( N e. _om /\ 2o C_ N ) /\ y e. ( _V X. U ) ) -> ( rec ( F , <. N , y >. ) ` N ) = ( rec ( F , <. U. N , ( 1st ` y ) >. ) ` U. N ) )