Theorem om2noseqrdg

Description: A helper lemma for the value of a recursive definition generator on a surreal sequence with characteristic function F ( x , y ) and initial value A . (Contributed by Scott Fenton, 18-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 ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) )
Assertion	om2noseqrdg	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ω ) → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )

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		fveq2	⊢ ( 𝑧 = ∅ → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ ∅ ) )
7		fveq2	⊢ ( 𝑧 = ∅ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∅ ) )
8		2fveq3	⊢ ( 𝑧 = ∅ → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) )
9	7 8	opeq12d	⊢ ( 𝑧 = ∅ → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ )
10	6 9	eqeq12d	⊢ ( 𝑧 = ∅ → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ ) )
11	10	imbi2d	⊢ ( 𝑧 = ∅ → ( ( 𝜑 → ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ) ↔ ( 𝜑 → ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ ) ) )
12		fveq2	⊢ ( 𝑧 = 𝑣 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ 𝑣 ) )
13		fveq2	⊢ ( 𝑧 = 𝑣 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑣 ) )
14		2fveq3	⊢ ( 𝑧 = 𝑣 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) )
15	13 14	opeq12d	⊢ ( 𝑧 = 𝑣 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ )
16	12 15	eqeq12d	⊢ ( 𝑧 = 𝑣 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) )
17	16	imbi2d	⊢ ( 𝑧 = 𝑣 → ( ( 𝜑 → ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ) ↔ ( 𝜑 → ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) )
18		fveq2	⊢ ( 𝑧 = suc 𝑣 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ suc 𝑣 ) )
19		fveq2	⊢ ( 𝑧 = suc 𝑣 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc 𝑣 ) )
20		2fveq3	⊢ ( 𝑧 = suc 𝑣 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) )
21	19 20	opeq12d	⊢ ( 𝑧 = suc 𝑣 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
22	18 21	eqeq12d	⊢ ( 𝑧 = suc 𝑣 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) )
23	22	imbi2d	⊢ ( 𝑧 = suc 𝑣 → ( ( 𝜑 → ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ) ↔ ( 𝜑 → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) ) )
24		fveq2	⊢ ( 𝑧 = 𝐵 → ( 𝑅 ‘ 𝑧 ) = ( 𝑅 ‘ 𝐵 ) )
25		fveq2	⊢ ( 𝑧 = 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐵 ) )
26		2fveq3	⊢ ( 𝑧 = 𝐵 → ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) = ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) )
27	25 26	opeq12d	⊢ ( 𝑧 = 𝐵 → ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )
28	24 27	eqeq12d	⊢ ( 𝑧 = 𝐵 → ( ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ↔ ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ ) )
29	28	imbi2d	⊢ ( 𝑧 = 𝐵 → ( ( 𝜑 → ( 𝑅 ‘ 𝑧 ) = ⟨ ( 𝐺 ‘ 𝑧 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑧 ) ) ⟩ ) ↔ ( 𝜑 → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ ) ) )
30	5	fveq1d	⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) )
31		opex	⊢ ⟨ 𝐶 , 𝐴 ⟩ ∈ V
32		fr0g	⊢ ( ⟨ 𝐶 , 𝐴 ⟩ ∈ V → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
33	31 32	ax-mp	⊢ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩
34	30 33	eqtrdi	⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = ⟨ 𝐶 , 𝐴 ⟩ )
35	1 2	om2noseq0	⊢ ( 𝜑 → ( 𝐺 ‘ ∅ ) = 𝐶 )
36	34	fveq2d	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ ) )
37		op2ndg	⊢ ( ( 𝐶 ∈ No ∧ 𝐴 ∈ 𝑉 ) → ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ ) = 𝐴 )
38	1 4 37	syl2anc	⊢ ( 𝜑 → ( 2nd ‘ ⟨ 𝐶 , 𝐴 ⟩ ) = 𝐴 )
39	36 38	eqtrd	⊢ ( 𝜑 → ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) = 𝐴 )
40	35 39	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ = ⟨ 𝐶 , 𝐴 ⟩ )
41	34 40	eqtr4d	⊢ ( 𝜑 → ( 𝑅 ‘ ∅ ) = ⟨ ( 𝐺 ‘ ∅ ) , ( 2nd ‘ ( 𝑅 ‘ ∅ ) ) ⟩ )
42		frsuc	⊢ ( 𝑣 ∈ ω → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
44	5	fveq1d	⊢ ( 𝜑 → ( 𝑅 ‘ suc 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) )
45	44	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → ( 𝑅 ‘ suc 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ suc 𝑣 ) )
46	5	fveq1d	⊢ ( 𝜑 → ( 𝑅 ‘ 𝑣 ) = ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) )
47	46	fveq2d	⊢ ( 𝜑 → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
48	47	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) , ⟨ 𝐶 , 𝐴 ⟩ ) ↾ ω ) ‘ 𝑣 ) ) )
49	43 45 48	3eqtr4d	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → ( 𝑅 ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) )
50	49	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 𝑅 ‘ suc 𝑣 ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) )
51		fveq2	⊢ ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) )
52		df-ov	⊢ ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ )
53		fvex	⊢ ( 𝐺 ‘ 𝑣 ) ∈ V
54		fvex	⊢ ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ∈ V
55		oveq1	⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ( 𝑤 +s 1s ) = ( ( 𝐺 ‘ 𝑣 ) +s 1s ) )
56		oveq1	⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ( 𝑤 𝐹 𝑧 ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) )
57	55 56	opeq12d	⊢ ( 𝑤 = ( 𝐺 ‘ 𝑣 ) → ⟨ ( 𝑤 +s 1s ) , ( 𝑤 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) ⟩ )
58		oveq2	⊢ ( 𝑧 = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) → ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) )
59	58	opeq2d	⊢ ( 𝑧 = ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) → ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 𝑧 ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
60		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 +s 1s ) = ( 𝑤 +s 1s ) )
61		oveq1	⊢ ( 𝑥 = 𝑤 → ( 𝑥 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑦 ) )
62	60 61	opeq12d	⊢ ( 𝑥 = 𝑤 → ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 +s 1s ) , ( 𝑤 𝐹 𝑦 ) ⟩ )
63		oveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑤 𝐹 𝑦 ) = ( 𝑤 𝐹 𝑧 ) )
64	63	opeq2d	⊢ ( 𝑦 = 𝑧 → ⟨ ( 𝑤 +s 1s ) , ( 𝑤 𝐹 𝑦 ) ⟩ = ⟨ ( 𝑤 +s 1s ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
65	62 64	cbvmpov	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) = ( 𝑤 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑤 +s 1s ) , ( 𝑤 𝐹 𝑧 ) ⟩ )
66		opex	⊢ ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ∈ V
67	57 59 65 66	ovmpo	⊢ ( ( ( 𝐺 ‘ 𝑣 ) ∈ V ∧ ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ∈ V ) → ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
68	53 54 67	mp2an	⊢ ( ( 𝐺 ‘ 𝑣 ) ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩
69	52 68	eqtr3i	⊢ ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩
70	51 69	eqtrdi	⊢ ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
71	70	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 𝐹 𝑦 ) ⟩ ) ‘ ( 𝑅 ‘ 𝑣 ) ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
72	50 71	eqtrd	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
73	1	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → 𝐶 ∈ No )
74	2	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
75		simpr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → 𝑣 ∈ ω )
76	73 74 75	om2noseqsuc	⊢ ( ( 𝜑 ∧ 𝑣 ∈ ω ) → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) +s 1s ) )
77	76	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 𝐺 ‘ suc 𝑣 ) = ( ( 𝐺 ‘ 𝑣 ) +s 1s ) )
78	72	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( 2nd ‘ ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ) )
79		ovex	⊢ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) ∈ V
80		ovex	⊢ ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ∈ V
81	79 80	op2nd	⊢ ( 2nd ‘ ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) )
82	78 81	eqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) = ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) )
83	77 82	opeq12d	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ = ⟨ ( ( 𝐺 ‘ 𝑣 ) +s 1s ) , ( ( 𝐺 ‘ 𝑣 ) 𝐹 ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ) ⟩ )
84	72 83	eqtr4d	⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ω ∧ ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) ) → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ )
85	84	exp32	⊢ ( 𝜑 → ( 𝑣 ∈ ω → ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) ) )
86	85	com12	⊢ ( 𝑣 ∈ ω → ( 𝜑 → ( ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) ) )
87	86	a2d	⊢ ( 𝑣 ∈ ω → ( ( 𝜑 → ( 𝑅 ‘ 𝑣 ) = ⟨ ( 𝐺 ‘ 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ 𝑣 ) ) ⟩ ) → ( 𝜑 → ( 𝑅 ‘ suc 𝑣 ) = ⟨ ( 𝐺 ‘ suc 𝑣 ) , ( 2nd ‘ ( 𝑅 ‘ suc 𝑣 ) ) ⟩ ) ) )
88	11 17 23 29 41 87	finds	⊢ ( 𝐵 ∈ ω → ( 𝜑 → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ ) )
89	88	impcom	⊢ ( ( 𝜑 ∧ 𝐵 ∈ ω ) → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )