This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem om2uzrdg

Description: A helper lemma for the value of a recursive definition generator on upper integers (typically either NN or NN0 ) with characteristic function F ( x , y ) and initial value A . Normally F is a function on the partition, and A is a member of the partition. See also comment in om2uz0i . (Contributed by Mario Carneiro, 26-Jun-2013) (Revised by Mario Carneiro, 18-Nov-2014)

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

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 fveq2 ⊢ ( 𝑧 = ∅ → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ ∅ ) )
6 fveq2 ⊢ ( 𝑧 = ∅ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∅ ) )
7 2fveq3 ⊢ ( 𝑧 = ∅ → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) )
8 6 7 opeq12d ⊢ ( 𝑧 = ∅ → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ )
9 5 8 eqeq12d ⊢ ( 𝑧 = ∅ → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ ) )
10 fveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ 𝑣 ) )
11 fveq2 ⊢ ( 𝑧 = 𝑣 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑣 ) )
12 2fveq3 ⊢ ( 𝑧 = 𝑣 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) )
13 11 12 opeq12d ⊢ ( 𝑧 = 𝑣 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ )
14 10 13 eqeq12d ⊢ ( 𝑧 = 𝑣 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) )
15 fveq2 ⊢ ( 𝑧 = suc 𝑣 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ suc 𝑣 ) )
16 fveq2 ⊢ ( 𝑧 = suc 𝑣 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc 𝑣 ) )
17 2fveq3 ⊢ ( 𝑧 = suc 𝑣 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) )
18 16 17 opeq12d ⊢ ( 𝑧 = suc 𝑣 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
19 15 18 eqeq12d ⊢ ( 𝑧 = suc 𝑣 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) )
20 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ 𝐵 ) )
21 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐵 ) )
22 2fveq3 ⊢ ( 𝑧 = 𝐵 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) )
23 21 22 opeq12d ⊢ ( 𝑧 = 𝐵 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )
24 20 23 eqeq12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ ) )
25 4 fveq1i ⊢ ( 𝑅 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ )
26 opex ⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ V
27 fr0g ⊢ ( ⟨ 𝐶 , 𝐴 ⟩ ∈ V → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
28 26 27 ax-mp ⊢ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
29 25 28 eqtri ⊢ ( 𝑅 ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
30 1 2 om2uz0i ⊢ ( 𝐺 ‘ ∅ ) = 𝐶
31 29 fveq2i ⊢ ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ )
32 1 elexi ⊢ 𝐶 ∈ V
33 32 3 op2nd ⊢ ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ ) = 𝐴
34 31 33 eqtri ⊢ ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = 𝐴
35 30 34 opeq12i ⊢ ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ = ⟨ 𝐶 , 𝐴 ⟩
36 29 35 eqtr4i ⊢ ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩
37 frsuc ⊢ ( 𝑣 ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
38 4 fveq1i ⊢ ( 𝑅 ‘ suc 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 )
39 4 fveq1i ⊢ ( 𝑅 ‘ 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 )
40 39 fveq2i ⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) )
41 37 38 40 3eqtr4g ⊢ ( 𝑣 ∈ ω → ( 𝑅 ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) )
42 fveq2 ⊢ ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) )
43 df-ov ⊢ ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ )
44 fvex ⊢ ( 𝐺 ‘ 𝑣 ) ∈ V
45 fvex ⊢ ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ∈ V
46 oveq1 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ( 𝑤 + 1 ) = ( ( 𝐺 ‘ 𝑣 ) + 1 ) )
47 oveq1 ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ( 𝑤 𝐹 𝑧 ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) )
48 46 47 opeq12d ⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) ⟩ )
49 oveq2 ⊢ ( 𝑧 = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) → ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) )
50 49 opeq2d ⊢ ( 𝑧 = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) → ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
51 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 + 1 ) = ( 𝑤 + 1 ) )
52 oveq1 ⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑦 ) )
53 51 52 opeq12d ⊢ ( 𝑥 = 𝑤 → ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑦 ) ⟩ )
54 oveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑤 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑧 ) )
55 54 opeq2d ⊢ ( 𝑦 = 𝑧 → ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
56 53 55 cbvmpov ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑤 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑤 + 1 ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
57 opex ⊢ ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ∈ V
58 48 50 56 57 ovmpo ⊢ ( ( ( 𝐺 ‘ 𝑣 ) ∈ V ∧ ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ∈ V ) → ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
59 44 45 58 mp2an ⊢ ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩
60 43 59 eqtr3i ⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩
61 42 60 eqtrdi ⊢ ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 + 1 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
62 41 61 sylan9eq ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
63 1 2 om2uzsuci ⊢ ( 𝑣 ∈ ω → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) + 1 ) )
64 63 adantr ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) + 1 ) )
65 62 fveq2d ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( 2nd ‘ ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ) )
66 ovex ⊢ ( ( 𝐺 ‘ 𝑣 ) + 1 ) ∈ V
67 ovex ⊢ ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ∈ V
68 66 67 op2nd ⊢ ( 2nd ‘ ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) )
69 65 68 eqtrdi ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) )
70 64 69 opeq12d ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) + 1 ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
71 62 70 eqtr4d ⊢ ( ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
72 71 ex ⊢ ( 𝑣 ∈ ω → ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) )
73 9 14 19 24 36 72 finds ⊢ ( 𝐵 ∈ ω → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )