Theorem om2noseqsuc

Description: The value of G at a successor. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
	om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
	om2noseqsuc.3	⊢ ( 𝜑 → 𝐴 ∈ ω )
Assertion	om2noseqsuc	⊢ ( 𝜑 → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )

Proof

Step	Hyp	Ref	Expression
1		om2noseq.1	⊢ ( 𝜑 → 𝐶 ∈ No )
2		om2noseq.2	⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3		om2noseqsuc.3	⊢ ( 𝜑 → 𝐴 ∈ ω )
4		ovex	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) ∈ V
5		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω )
6		oveq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 +s 1s ) = ( 𝑥 +s 1s ) )
7		oveq1	⊢ ( 𝑦 = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) → ( 𝑦 +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) )
8	5 6 7	frsucmpt2	⊢ ( ( 𝐴 ∈ ω ∧ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) ∈ V ) → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ suc 𝐴 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) )
9	3 4 8	sylancl	⊢ ( 𝜑 → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ suc 𝐴 ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) )
10	2	fveq1d	⊢ ( 𝜑 → ( 𝐺 ‘ suc 𝐴 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ suc 𝐴 ) )
11	2	fveq1d	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐴 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) )
12	11	oveq1d	⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝐴 ) +s 1s ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) ‘ 𝐴 ) +s 1s ) )
13	9 10 12	3eqtr4d	⊢ ( 𝜑 → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )