Definition df-seqs 28280

Description: Define a general-purpose sequence builder for surreal numbers. Compare df-seq 14039. 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 28279	. 2 class seqs𝑀( + , 𝐹)
5		vx	. . . . 5 setvar 𝑥
6		vy	. . . . 5 setvar 𝑦
7		cvv 3479	. . . . 5 class V
8	5	cv 1539	. . . . . . 7 class 𝑥
9		c1s 27858	. . . . . . 7 class 1s
10		cadds 27982	. . . . . . 7 class +s
11	8, 9, 10	co 7429	. . . . . 6 class (𝑥 +s 1s )
12	6	cv 1539	. . . . . . 7 class 𝑦
13	11, 2	cfv 6559	. . . . . . 7 class (𝐹‘(𝑥 +s 1s ))
14	12, 13, 1	co 7429	. . . . . 6 class (𝑦 + (𝐹‘(𝑥 +s 1s )))
15	11, 14	cop 4630	. . . . 5 class ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩
16	5, 6, 7, 7, 15	cmpo 7431	. . . 4 class (𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩)
17	3, 2	cfv 6559	. . . . 5 class (𝐹‘𝑀)
18	3, 17	cop 4630	. . . 4 class ⟨𝑀, (𝐹‘𝑀)⟩
19	16, 18	crdg 8445	. . 3 class rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩)
20		com 7883	. . 3 class ω
21	19, 20	cima 5686	. 2 class (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)
22	4, 21	wceq 1540	1 wff seqs𝑀( + , 𝐹) = (rec((𝑥 ∈ V, 𝑦 ∈ V ↦ ⟨(𝑥 +s 1s ), (𝑦 + (𝐹‘(𝑥 +s 1s )))⟩), ⟨𝑀, (𝐹‘𝑀)⟩) “ ω)

This definition is referenced by:  seqsex  28281  seqseq123d  28282  nfseqs  28283  seqsval  28284