Metamath Proof Explorer


Theorem finxpreclem4

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

Ref Expression
Hypothesis finxpreclem4.1 F = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x
Assertion finxpreclem4 N ω 2 𝑜 N y V × U rec F N y N = rec F N 1 st y N

Proof

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