Metamath Proof Explorer

Theorem rdgeqoa

Description: If a recursive function with an initial value A at step N is equal to itself with an initial value B at step M , then every finite number of successor steps will also be equal. (Contributed by ML, 21-Oct-2020)

Ref Expression
Assertion rdgeqoa ⊢N∈On∧M∈On∧X∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X

Proof

Step Hyp Ref Expression
1 simp3 ⊢N∈On∧M∈On∧X∈ω→X∈ω
2 eleq1 ⊢x=X→x∈ω↔X∈ω
3 2 3anbi3d ⊢x=X→N∈On∧M∈On∧x∈ω↔N∈On∧M∈On∧X∈ω
4 oveq2 ⊢x=X→N+𝑜x=N+𝑜X
5 4 fveq2d ⊢x=X→rec⁡FA⁡N+𝑜x=rec⁡FA⁡N+𝑜X
6 oveq2 ⊢x=X→M+𝑜x=M+𝑜X
7 6 fveq2d ⊢x=X→rec⁡FB⁡M+𝑜x=rec⁡FB⁡M+𝑜X
8 5 7 eqeq12d ⊢x=X→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X
9 8 imbi2d ⊢x=X→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X
10 3 9 imbi12d ⊢x=X→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔N∈On∧M∈On∧X∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X
11 peano1 ⊢∅∈ω
12 oa0 ⊢N∈On→N+𝑜∅=N
13 12 fveq2d ⊢N∈On→rec⁡FA⁡N+𝑜∅=rec⁡FA⁡N
14 13 eqcomd ⊢N∈On→rec⁡FA⁡N=rec⁡FA⁡N+𝑜∅
15 oa0 ⊢M∈On→M+𝑜∅=M
16 15 fveq2d ⊢M∈On→rec⁡FB⁡M+𝑜∅=rec⁡FB⁡M
17 16 eqcomd ⊢M∈On→rec⁡FB⁡M=rec⁡FB⁡M+𝑜∅
18 14 17 eqeqan12d ⊢N∈On∧M∈On→rec⁡FA⁡N=rec⁡FB⁡M↔rec⁡FA⁡N+𝑜∅=rec⁡FB⁡M+𝑜∅
19 18 biimpd ⊢N∈On∧M∈On→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜∅=rec⁡FB⁡M+𝑜∅
20 eleq1 ⊢x=∅→x∈ω↔∅∈ω
21 20 3anbi3d ⊢x=∅→N∈On∧M∈On∧x∈ω↔N∈On∧M∈On∧∅∈ω
22 11 biantru ⊢M∈On↔M∈On∧∅∈ω
23 22 anbi2i ⊢N∈On∧M∈On↔N∈On∧M∈On∧∅∈ω
24 3anass ⊢N∈On∧M∈On∧∅∈ω↔N∈On∧M∈On∧∅∈ω
25 23 24 bitr4i ⊢N∈On∧M∈On↔N∈On∧M∈On∧∅∈ω
26 21 25 bitr4di ⊢x=∅→N∈On∧M∈On∧x∈ω↔N∈On∧M∈On
27 oveq2 ⊢x=∅→N+𝑜x=N+𝑜∅
28 27 fveq2d ⊢x=∅→rec⁡FA⁡N+𝑜x=rec⁡FA⁡N+𝑜∅
29 oveq2 ⊢x=∅→M+𝑜x=M+𝑜∅
30 29 fveq2d ⊢x=∅→rec⁡FB⁡M+𝑜x=rec⁡FB⁡M+𝑜∅
31 28 30 eqeq12d ⊢x=∅→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N+𝑜∅=rec⁡FB⁡M+𝑜∅
32 31 imbi2d ⊢x=∅→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜∅=rec⁡FB⁡M+𝑜∅
33 26 32 imbi12d ⊢x=∅→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔N∈On∧M∈On→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜∅=rec⁡FB⁡M+𝑜∅
34 19 33 mpbiri ⊢x=∅→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
35 34 ax-gen ⊢∀xx=∅→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
36 sbc6g ⊢∅∈ω→[˙∅/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔∀xx=∅→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
37 35 36 mpbiri ⊢∅∈ω→[˙∅/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
38 11 37 ax-mp ⊢[˙∅/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
39 peano2b ⊢x∈ω↔suc⁡x∈ω
40 39 3anbi3i ⊢N∈On∧M∈On∧x∈ω↔N∈On∧M∈On∧suc⁡x∈ω
41 40 imbi1i ⊢N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
42 nnon ⊢x∈ω→x∈On
43 oacl ⊢N∈On∧x∈On→N+𝑜x∈On
44 oacl ⊢M∈On∧x∈On→M+𝑜x∈On
45 43 44 anim12i ⊢N∈On∧x∈On∧M∈On∧x∈On→N+𝑜x∈On∧M+𝑜x∈On
46 45 3impdir ⊢N∈On∧M∈On∧x∈On→N+𝑜x∈On∧M+𝑜x∈On
47 rdgsuc ⊢N+𝑜x∈On→rec⁡FA⁡suc⁡N+𝑜x=F⁡rec⁡FA⁡N+𝑜x
48 fveq2 ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→F⁡rec⁡FA⁡N+𝑜x=F⁡rec⁡FB⁡M+𝑜x
49 47 48 sylan9eqr ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x∧N+𝑜x∈On→rec⁡FA⁡suc⁡N+𝑜x=F⁡rec⁡FB⁡M+𝑜x
50 49 adantrr ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x∧N+𝑜x∈On∧M+𝑜x∈On→rec⁡FA⁡suc⁡N+𝑜x=F⁡rec⁡FB⁡M+𝑜x
51 rdgsuc ⊢M+𝑜x∈On→rec⁡FB⁡suc⁡M+𝑜x=F⁡rec⁡FB⁡M+𝑜x
52 51 ad2antll ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x∧N+𝑜x∈On∧M+𝑜x∈On→rec⁡FB⁡suc⁡M+𝑜x=F⁡rec⁡FB⁡M+𝑜x
53 50 52 eqtr4d ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x∧N+𝑜x∈On∧M+𝑜x∈On→rec⁡FA⁡suc⁡N+𝑜x=rec⁡FB⁡suc⁡M+𝑜x
54 46 53 sylan2 ⊢rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x∧N∈On∧M∈On∧x∈On→rec⁡FA⁡suc⁡N+𝑜x=rec⁡FB⁡suc⁡M+𝑜x
55 54 ancoms ⊢N∈On∧M∈On∧x∈On∧rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡suc⁡N+𝑜x=rec⁡FB⁡suc⁡M+𝑜x
56 42 55 syl3anl3 ⊢N∈On∧M∈On∧x∈ω∧rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡suc⁡N+𝑜x=rec⁡FB⁡suc⁡M+𝑜x
57 onasuc ⊢N∈On∧x∈ω→N+𝑜suc⁡x=suc⁡N+𝑜x
58 57 fveq2d ⊢N∈On∧x∈ω→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FA⁡suc⁡N+𝑜x
59 58 3adant2 ⊢N∈On∧M∈On∧x∈ω→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FA⁡suc⁡N+𝑜x
60 59 adantr ⊢N∈On∧M∈On∧x∈ω∧rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FA⁡suc⁡N+𝑜x
61 onasuc ⊢M∈On∧x∈ω→M+𝑜suc⁡x=suc⁡M+𝑜x
62 61 fveq2d ⊢M∈On∧x∈ω→rec⁡FB⁡M+𝑜suc⁡x=rec⁡FB⁡suc⁡M+𝑜x
63 62 3adant1 ⊢N∈On∧M∈On∧x∈ω→rec⁡FB⁡M+𝑜suc⁡x=rec⁡FB⁡suc⁡M+𝑜x
64 63 adantr ⊢N∈On∧M∈On∧x∈ω∧rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FB⁡M+𝑜suc⁡x=rec⁡FB⁡suc⁡M+𝑜x
65 56 60 64 3eqtr4d ⊢N∈On∧M∈On∧x∈ω∧rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
66 65 ex ⊢N∈On∧M∈On∧x∈ω→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
67 66 imim2d ⊢N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
68 40 67 sylbir ⊢N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
69 68 a2i ⊢N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
70 41 69 sylbi ⊢N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
71 sbcimg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
72 sbc3an ⊢[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω↔[˙suc⁡x/x]˙N∈On∧[˙suc⁡x/x]˙M∈On∧[˙suc⁡x/x]˙x∈ω
73 sbcg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On↔N∈On
74 sbcg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙M∈On↔M∈On
75 sbcel1v ⊢[˙suc⁡x/x]˙x∈ω↔suc⁡x∈ω
76 75 a1i ⊢suc⁡x∈ω→[˙suc⁡x/x]˙x∈ω↔suc⁡x∈ω
77 73 74 76 3anbi123d ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On∧[˙suc⁡x/x]˙M∈On∧[˙suc⁡x/x]˙x∈ω↔N∈On∧M∈On∧suc⁡x∈ω
78 72 77 bitrid ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω↔N∈On∧M∈On∧suc⁡x∈ω
79 sbcimg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→[˙suc⁡x/x]˙rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
80 sbcg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M↔rec⁡FA⁡N=rec⁡FB⁡M
81 sbceqg ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔⦋suc⁡x/x⦌rec⁡FA⁡N+𝑜x=⦋suc⁡x/x⦌rec⁡FB⁡M+𝑜x
82 csbfv12 ⊢⦋suc⁡x/x⦌rec⁡FA⁡N+𝑜x=⦋suc⁡x/x⦌rec⁡FA⁡⦋suc⁡x/x⦌N+𝑜x
83 csbconstg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FA=rec⁡FA
84 csbov123 ⊢⦋suc⁡x/x⦌N+𝑜x=⦋suc⁡x/x⦌N⦋suc⁡x/x⦌+𝑜⦋suc⁡x/x⦌x
85 csbconstg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌+𝑜=+𝑜
86 csbconstg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌N=N
87 csbvarg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌x=suc⁡x
88 85 86 87 oveq123d ⊢suc⁡x∈ω→⦋suc⁡x/x⦌N⦋suc⁡x/x⦌+𝑜⦋suc⁡x/x⦌x=N+𝑜suc⁡x
89 84 88 eqtrid ⊢suc⁡x∈ω→⦋suc⁡x/x⦌N+𝑜x=N+𝑜suc⁡x
90 83 89 fveq12d ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FA⁡⦋suc⁡x/x⦌N+𝑜x=rec⁡FA⁡N+𝑜suc⁡x
91 82 90 eqtrid ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FA⁡N+𝑜x=rec⁡FA⁡N+𝑜suc⁡x
92 csbfv12 ⊢⦋suc⁡x/x⦌rec⁡FB⁡M+𝑜x=⦋suc⁡x/x⦌rec⁡FB⁡⦋suc⁡x/x⦌M+𝑜x
93 csbconstg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FB=rec⁡FB
94 csbov123 ⊢⦋suc⁡x/x⦌M+𝑜x=⦋suc⁡x/x⦌M⦋suc⁡x/x⦌+𝑜⦋suc⁡x/x⦌x
95 csbconstg ⊢suc⁡x∈ω→⦋suc⁡x/x⦌M=M
96 85 95 87 oveq123d ⊢suc⁡x∈ω→⦋suc⁡x/x⦌M⦋suc⁡x/x⦌+𝑜⦋suc⁡x/x⦌x=M+𝑜suc⁡x
97 94 96 eqtrid ⊢suc⁡x∈ω→⦋suc⁡x/x⦌M+𝑜x=M+𝑜suc⁡x
98 93 97 fveq12d ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FB⁡⦋suc⁡x/x⦌M+𝑜x=rec⁡FB⁡M+𝑜suc⁡x
99 92 98 eqtrid ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FB⁡M+𝑜x=rec⁡FB⁡M+𝑜suc⁡x
100 91 99 eqeq12d ⊢suc⁡x∈ω→⦋suc⁡x/x⦌rec⁡FA⁡N+𝑜x=⦋suc⁡x/x⦌rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
101 81 100 bitrd ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
102 80 101 imbi12d ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→[˙suc⁡x/x]˙rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
103 79 102 bitrd ⊢suc⁡x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
104 78 103 imbi12d ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→[˙suc⁡x/x]˙rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
105 71 104 bitrd ⊢suc⁡x∈ω→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x↔N∈On∧M∈On∧suc⁡x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜suc⁡x=rec⁡FB⁡M+𝑜suc⁡x
106 70 105 imbitrrid ⊢suc⁡x∈ω→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
107 39 106 sylbi ⊢x∈ω→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x→[˙suc⁡x/x]˙N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
108 38 107 findes ⊢x∈ω→N∈On∧M∈On∧x∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜x=rec⁡FB⁡M+𝑜x
109 10 108 vtoclga ⊢X∈ω→N∈On∧M∈On∧X∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X
110 1 109 mpcom ⊢N∈On∧M∈On∧X∈ω→rec⁡FA⁡N=rec⁡FB⁡M→rec⁡FA⁡N+𝑜X=rec⁡FB⁡M+𝑜X