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	⊢ ( 𝐵 ∈ ω → ( 𝑅 ‘ 𝐵 ) = ⟨ ( 𝐺 ‘ 𝐵 ) , ( 2^nd ‘ ( 𝑅 ‘ 𝐵 ) ) ⟩ )

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

Metamath Proof Explorer

Theorem om2uzrdg

Proof