df-seqom

Description: Index-aware recursive definitions over _om . A mashup of df-rdg and df-seq , this allows for recursive definitions that use an index in the recursion in cases where Infinity is not admitted. (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Assertion	df-seqom	$⊢ {seq}_{ω} (F, I) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) [ω]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$class F$
1		cI	$class I$
2	0 1	cseqom	$class {seq}_{ω} (F, I)$
3		vi	$setvar i$
4		com	$class ω$
5		vv	$setvar v$
6		cvv	$class V$
7	3	cv	$setvar i$
8	7	csuc	$class suc i$
9	5	cv	$setvar v$
10	7 9 0	co	$class (i F v)$
11	8 10	cop	$class ⟨suc i, i F v⟩$
12	3 5 4 6 11	cmpo	$class (i \in ω, v \in V ⟼ ⟨suc i, i F v⟩)$
13		c0	$class \emptyset$
14		cid	$class I$
15	1 14	cfv	$class I (I)$
16	13 15	cop	$class ⟨\emptyset, I (I)⟩$
17	12 16	crdg	$class rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩)$
18	17 4	cima	$class rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) [ω]$
19	2 18	wceq	$wff {seq}_{ω} (F, I) = rec ((i \in ω, v \in V ⟼ ⟨suc i, i F v⟩), ⟨\emptyset, I (I)⟩) [ω]$

Metamath Proof Explorer

Definition df-seqom

Detailed syntax breakdown