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 e. On /\ M e. On /\ X e. _om ) -> ( ( rec ( F , A ) ` N ) = ( rec ( F , B ) ` M ) -> ( rec ( F , A ) ` ( N +o X ) ) = ( rec ( F , B ) ` ( M +o X ) ) ) )

Proof

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