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 ( ( 𝑁 ∈ On ∧ 𝑀 ∈ On ∧ 𝑋 ∈ ω ) → ( ( rec ( 𝐹 , 𝐴 ) ‘ 𝑁 ) = ( rec ( 𝐹 , 𝐵 ) ‘ 𝑀 ) → ( rec ( 𝐹 , 𝐴 ) ‘ ( 𝑁 +o 𝑋 ) ) = ( rec ( 𝐹 , 𝐵 ) ‘ ( 𝑀 +o 𝑋 ) ) ) )

Proof

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