Definition df-seqs 28258

Description: Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14022. Note that in the theorems we develop here, we do not require 𝑀 to be an integer. This is because there are infinite surreal numbers and we may want to start our sequence there. (Contributed by Scott Fenton, 18-Apr-2025.)

Assertion

Ref	Expression
df-seqs	⊢ seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)

Distinct variable groups:   𝑥, + ,𝑦   𝑥,𝑀,𝑦   𝑥,𝐹,𝑦

Detailed syntax breakdown of Definition df-seqs

Step	Hyp	Ref	Expression
1		c.pl	. . 3 class +
2		cF	. . 3 class 𝐹
3		cM	. . 3 class 𝑀
4	1, 2, 3	cseqs 28257	. 2 class seqs𝑀( + , 𝐹)
5		vx	. . . . 5 setvar 𝑥
6		vy	. . . . 5 setvar 𝑦
7		cvv 3462	. . . . 5 class V
8	5	cv 1533	. . . . . . 7 class 𝑥
9		c1s 27853	. . . . . . 7 class 1s
10		cadds 27973	. . . . . . 7 class +s
11	8, 9, 10	co 7424	. . . . . 6 class (𝑥 +s 1s )
12	6	cv 1533	. . . . . . 7 class 𝑦
13	11, 2	cfv 6554	. . . . . . 7 class (𝐹‘(𝑥 +s 1s ))
14	12, 13, 1	co 7424	. . . . . 6 class (𝑦 + (𝐹‘(𝑥 +s 1s )))
15	11, 14	cop 4639	. . . . 5 class ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩
16	5, 6, 7, 7, 15	cmpo 7426	. . . 4 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩)
17	3, 2	cfv 6554	. . . . 5 class (𝐹‘𝑀)
18	3, 17	cop 4639	. . . 4 class ⟨𝑀, (𝐹‘𝑀)⟩
19	16, 18	crdg 8439	. . 3 class rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
20		com 7876	. . 3 class ω
21	19, 20	cima 5685	. 2 class (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
22	4, 21	wceq 1534	1 wff seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)

This definition is referenced by:  seqsex  28259  seqseq123d  28260  nfseqs  28261  seqsval  28262