om2noseqsuc

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

Step	Hyp	Ref	Expression
1		om2noseq.1	$⊢ φ \to C \in No$
2		om2noseq.2	$⊢ φ \to G = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
3		om2noseqsuc.3	$⊢ φ \to A \in ω$
4		ovex	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s} \in V$
5		eqid	$⊢ {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω} = {rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}$
6		oveq1	$⊢ y = x \to y +_{s} 1_{s} = x +_{s} 1_{s}$
7		oveq1	$⊢ y = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) \to y +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s}$
8	5 6 7	frsucmpt2	$⊢ (A \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s} \in V) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (suc A) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s}$
9	3 4 8	sylancl	$⊢ φ \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (suc A) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s}$
10	2	fveq1d	$⊢ φ \to G (suc A) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (suc A)$
11	2	fveq1d	$⊢ φ \to G (A) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A)$
12	11	oveq1d	$⊢ φ \to G (A) +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), C) ↾}_{ω}) (A) +_{s} 1_{s}$
13	9 10 12	3eqtr4d	$⊢ φ \to G (suc A) = G (A) +_{s} 1_{s}$

Metamath Proof Explorer