Metamath Proof Explorer

Definition 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 ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ 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 ∈ ω , v ∈ V ⟼ suc ⁡ i i F v
13 c0 class ∅
14 cid class I
15 1 14 cfv class I ⁡ I
16 13 15 cop class ∅ I ⁡ I
17 12 16 crdg class rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I
18 17 4 cima class rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ω
19 2 18 wceq wff seq ω F I = rec ⁡ i ∈ ω , v ∈ V ⟼ suc ⁡ i i F v ∅ I ⁡ I ω