Theorem om2uzsuci

Description: The value of G (see om2uz0i ) at a successor. (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

	Ref	Expression
Hypotheses	om2uz.1	⊢ 𝐶 ∈ ℤ
	om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion	om2uzsuci	⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) )

Proof

Step	Hyp	Ref	Expression
1		om2uz.1	⊢ 𝐶 ∈ ℤ
2		om2uz.2	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3		suceq	⊢ ( 𝑧 = 𝐴 → suc 𝑧 = suc 𝐴 )
4	3	fveq2d	⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ suc 𝑧 ) = ( 𝐺 ‘ suc 𝐴 ) )
5		fveq2	⊢ ( 𝑧 = 𝐴 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐴 ) )
6	5	oveq1d	⊢ ( 𝑧 = 𝐴 → ( ( 𝐺 ‘ 𝑧 ) + 1 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) )
7	4 6	eqeq12d	⊢ ( 𝑧 = 𝐴 → ( ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) ↔ ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) ) )
8		ovex	⊢ ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ V
9		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 + 1 ) = ( 𝑥 + 1 ) )
10		oveq1	⊢ ( 𝑦 = ( 𝐺 ‘ 𝑧 ) → ( 𝑦 + 1 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
11	2 9 10	frsucmpt2	⊢ ( ( 𝑧 ∈ ω ∧ ( ( 𝐺 ‘ 𝑧 ) + 1 ) ∈ V ) → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
12	8 11	mpan2	⊢ ( 𝑧 ∈ ω → ( 𝐺 ‘ suc 𝑧 ) = ( ( 𝐺 ‘ 𝑧 ) + 1 ) )
13	7 12	vtoclga	⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) + 1 ) )