seqomsuc

Description: Value of an index-aware recursive definition at a successor. (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Hypothesis	seqom.a	$⊢ G = {seq}_{ω} (F, I)$
	Assertion	seqomsuc	$⊢ A \in ω \to G (suc A) = A F G (A)$

Step	Hyp	Ref	Expression
1		seqom.a	$⊢ G = {seq}_{ω} (F, I)$
2		seqomlem0	$⊢ rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) = rec ((c \in ω, d \in V ⟼ ⟨suc c, c F d⟩), ⟨\emptyset, I (I)⟩)$
3	2	seqomlem4	$⊢ A \in ω \to rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] (suc A) = A F rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] (A)$
4		df-seqom	$⊢ {seq}_{ω} (F, I) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω]$
5	1 4	eqtri	$⊢ G = rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω]$
6	5	fveq1i	$⊢ G (suc A) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] (suc A)$
7	5	fveq1i	$⊢ G (A) = rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] (A)$
8	7	oveq2i	$⊢ A F G (A) = A F rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] (A)$
9	3 6 8	3eqtr4g	$⊢ A \in ω \to G (suc A) = A F G (A)$

Metamath Proof Explorer