Metamath Proof Explorer

Theorem noseqrdgsuc

Description: Successor value of a recursive definition generator on surreal sequences. (Contributed by Scott Fenton, 19-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
noseqrdg.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
noseqrdg.2 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
noseqrdg.3 ⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
Assertion noseqrdgsuc ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑆 ‘ ( 𝐵 +s 1s ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
2 om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3 om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4 noseqrdg.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
5 noseqrdg.2 ⊢ ( 𝜑 → 𝑅 = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
6 noseqrdg.3 ⊢ ( 𝜑 → 𝑆 = ran 𝑅 )
7 1 2 3 4 5 6 noseqrdgfn ⊢ ( 𝜑 → 𝑆 Fn 𝑍 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝑆 Fn 𝑍 )
9 8 fnfund ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → Fun 𝑆 )
10 3 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝐶 ∈ No )
12 simpr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝐵 ∈ 𝑍 )
13 10 11 12 noseqp1 ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐵 +s 1s ) ∈ 𝑍 )
14 1 2 3 4 5 noseqrdglem ⊢ ( ( 𝜑 ∧ ( 𝐵 +s 1s ) ∈ 𝑍 ) → ⟨ ( 𝐵 +s 1s ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) ⟩ ∈ ran 𝑅 )
15 13 14 syldan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ ( 𝐵 +s 1s ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) ⟩ ∈ ran 𝑅 )
16 6 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝑆 = ran 𝑅 )
17 15 16 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ ( 𝐵 +s 1s ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) ⟩ ∈ 𝑆 )
18 funopfv ⊢ ( Fun 𝑆 → ( ⟨ ( 𝐵 +s 1s ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) ⟩ ∈ 𝑆 → ( 𝑆 ‘ ( 𝐵 +s 1s ) ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) ) )
19 9 17 18 sylc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑆 ‘ ( 𝐵 +s 1s ) ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) )
20 1 2 3 om2noseqf1o ⊢ ( 𝜑 → 𝐺 : ω –1-1-onto→ 𝑍 )
21 20 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝐺 : ω –1-1-onto→ 𝑍 )
22 f1ocnvdm ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
23 20 22 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
24 peano2 ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω )
26 21 25 jca ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) )
27 2 adantr ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
28 11 27 23 om2noseqsuc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) )
29 f1ocnvfv2 ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
30 20 29 sylan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = 𝐵 )
31 30 oveq1d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) = ( 𝐵 +s 1s ) )
32 28 31 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( 𝐵 +s 1s ) )
33 f1ocnvfv ⊢ ( ( 𝐺 : ω –1-1-onto→ 𝑍 ∧ suc ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( 𝐺 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( 𝐵 +s 1s ) → ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) = suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
34 26 32 33 sylc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) = suc ( ◡ 𝐺 ‘ 𝐵 ) )
35 34 fveq2d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) = ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
36 35 fveq2d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ ( 𝐵 +s 1s ) ) ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
37 19 36 eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑆 ‘ ( 𝐵 +s 1s ) ) = ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
38 frsuc ⊢ ( ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
40 5 fveq1d ⊢ ( 𝜑 → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
41 40 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) )
42 5 fveq1d ⊢ ( 𝜑 → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) )
43 42 fveq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
44 43 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
45 39 41 44 3eqtr4d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
46 1 2 3 4 5 om2noseqrdg ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ) )
48 df-ov ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ )
49 47 48 eqtr4di ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
50 45 49 eqtrd ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
51 fvex ⊢ ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ V
52 fvex ⊢ ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ∈ V
53 oveq1 ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ( 𝑧 +s 1s ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) )
54 oveq1 ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ( 𝑧 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) )
55 53 54 opeq12d ⊢ ( 𝑧 = ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) → ⟨ ( 𝑧 +s 1s ) , ( 𝑧 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) ⟩ )
56 oveq2 ⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
57 56 opeq2d ⊢ ( 𝑤 = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) → ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 𝑤 ) ⟩ = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
58 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 +s 1s ) = ( 𝑧 +s 1s ) )
59 oveq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑦 ) )
60 58 59 opeq12d ⊢ ( 𝑥 = 𝑧 → ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 +s 1s ) , ( 𝑧 𝐹 𝑦 ) ⟩ )
61 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 𝐹 𝑦 ) = ( 𝑧 𝐹 𝑤 ) )
62 61 opeq2d ⊢ ( 𝑦 = 𝑤 → ⟨ ( 𝑧 +s 1s ) , ( 𝑧 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑧 +s 1s ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
63 60 62 cbvmpov ⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ⟨ ( 𝑧 +s 1s ) , ( 𝑧 𝐹 𝑤 ) ⟩ )
64 opex ⊢ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ∈ V
65 55 57 63 64 ovmpo ⊢ ( ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ∈ V ∧ ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ∈ V ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
66 51 52 65 mp2an ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩
67 50 66 eqtrdi ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) = ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ )
68 67 fveq2d ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ) )
69 ovex ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) ∈ V
70 ovex ⊢ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ∈ V
71 69 70 op2nd ⊢ ( 2nd ‘ ⟨ ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) +s 1s ) , ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) ⟩ ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
72 68 71 eqtrdi ⊢ ( ( 𝜑 ∧ ( ◡ 𝐺 ‘ 𝐵 ) ∈ ω ) → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
73 23 72 syldan ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 2nd ‘ ( 𝑅 ‘ suc ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
74 1 2 3 4 5 noseqrdglem ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ ran 𝑅 )
75 74 16 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ 𝑆 )
76 funopfv ⊢ ( Fun 𝑆 → ( ⟨ 𝐵 , ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ⟩ ∈ 𝑆 → ( 𝑆 ‘ 𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) )
77 9 75 76 sylc ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑆 ‘ 𝐵 ) = ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) )
78 77 eqcomd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) = ( 𝑆 ‘ 𝐵 ) )
79 30 78 oveq12d ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( ( 𝐺 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ ( ◡ 𝐺 ‘ 𝐵 ) ) ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )
80 37 73 79 3eqtrd ⊢ ( ( 𝜑 ∧ 𝐵 ∈ 𝑍 ) → ( 𝑆 ‘ ( 𝐵 +s 1s ) ) = ( 𝐵 𝐹 ( 𝑆 ‘ 𝐵 ) ) )