Metamath Proof Explorer

Theorem uzrdgsuci

Description: Successor value of a recursive definition generator on upper integers. See comment in om2uzrdg . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 ⊢ 𝐶 ∈ ℤ
om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
uzrdg.1 ⊢ 𝐴 ∈ V
uzrdg.2 ⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
uzrdg.3 ⊢ 𝑆 = ran 𝑅
Assertion uzrdgsuci ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ 𝐶 ∈ ℤ
2 om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 uzrdg.1 ⊢ 𝐴 ∈ V
4 uzrdg.2 ⊢ 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω )
5 uzrdg.3 ⊢ 𝑆 = ran 𝑅
6 1 2 3 4 5 uzrdgfni ⊢ 𝑆 Fn ( ℤ≥ ‘ 𝐶 )
7 fnfun ⊢ ( 𝑆 Fn ( ℤ≥ ‘ 𝐶 ) → Fun 𝑆 )
8 6 7 ax-mp ⊢ Fun 𝑆
9 peano2uz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
10 1 2 3 4 uzrdglem ⊢ ( ( 𝐵 + 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ ran 𝑅 )
11 9 10 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ ran 𝑅 )
12 11 5 eleqtrrdi ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ 𝑆 )
13 funopfv ⊢ ( Fun 𝑆 → ( ⟨ ( 𝐵 + 1 ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ⟩ ∈ 𝑆 → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) ) )
14 8 12 13 mpsyl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) )
15 1 2 om2uzf1oi ⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 )
16 f1ocnvdm ⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
17 15 16 mpan ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
18 peano2 ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
19 17 18 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
20 1 2 om2uzsuci ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) )
21 17 20 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) )
22 f1ocnvfv2 ⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
23 15 22 mpan ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
24 23 oveq1d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) = ( 𝐵 + 1 ) )
25 21 24 eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( 𝐵 + 1 ) )
26 f1ocnvfv ⊢ ( ( 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 𝐶 ) ∧ suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( 𝐵 + 1 ) → ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
27 15 26 mpan ⊢ ( suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( 𝐵 + 1 ) → ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
28 19 25 27 sylc ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) = suc ( ◡ 𝐺 ‘ 𝐵 ) )
29 28 fveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) = ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
30 29 fveq2d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 + 1 ) ) ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
31 14 30 eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
32 frsuc ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
33 4 fveq1i ⊢ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) )
34 4 fveq1i ⊢ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) )
35 34 fveq2i ⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) )
36 32 33 35 3eqtr4g ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
37 1 2 3 4 om2uzrdg ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
38 37 fveq2d ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ) )
39 df-ov ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
40 38 39 eqtr4di ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
41 36 40 eqtrd ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
42 fvex ⊢ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ V
43 fvex ⊢ ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ∈ V
44 oveq1 ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ( 𝑧 + 1 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) )
45 oveq1 ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ( 𝑧 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) )
46 44 45 opeq12d ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) ⟩ )
47 oveq2 ⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
48 47 opeq2d ⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) → ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
49 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 + 1 ) = ( 𝑧 + 1 ) )
50 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑦 ) )
51 49 50 opeq12d ⊢ ( 𝑥 = 𝑧 → ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑦 ) ⟩ )
52 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑤 ) )
53 52 opeq2d ⊢ ( 𝑦 = 𝑤 → ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
54 51 53 cbvmpov ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 + 1 ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
55 opex ⊢ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ∈ V
56 46 48 54 55 ovmpo ⊢ ( ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ V ∧ ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ∈ V ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
57 42 43 56 mp2an ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩
58 41 57 eqtrdi ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
59 58 fveq2d ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ) )
60 ovex ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) ∈ V
61 ovex ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ∈ V
62 60 61 op2nd ⊢ ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) + 1 ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
63 59 62 eqtrdi ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
64 17 63 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
65 1 2 3 4 uzrdglem ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )
66 65 5 eleqtrrdi ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ 𝑆 )
67 funopfv ⊢ ( Fun 𝑆 → ( ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ 𝑆 → ( 𝑆 ‘ 𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
68 8 66 67 mpsyl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑆 ‘ 𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
69 68 eqcomd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( 𝑆 ‘ 𝐵 ) )
70 23 69 oveq12d ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )
71 31 64 70 3eqtrd ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝑆 ‘ ( 𝐵 + 1 ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )