fnseqom

Description: An index-aware recursive definition defines a function on the natural numbers. (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Hypothesis	seqom.a	$⊢ G = {seq}_{ω} (F, I)$
	Assertion	fnseqom	$⊢ G Fn ω$

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	seqomlem2	$⊢ rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] Fn ω$
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	fneq1i	$⊢ G Fn ω \leftrightarrow rec ((a \in ω, b \in V ⟼ ⟨suc a, a F b⟩), ⟨\emptyset, I (I)⟩) [ω] Fn ω$
7	3 6	mpbir	$⊢ G Fn ω$

Metamath Proof Explorer