Definition df-seqs

Description: Define a general-purpose sequence builder for surreal numbers. Compare df-seq . Note that in the theorems we develop here, we do not require M 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)

	Ref	Expression
Assertion	df-seqs	|- seq_s M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	|- M
1		c.pl	|- .+
2		cF	|- F
3	1 2 0	cseqs	|- seq_s M ( .+ , F )
4		vx	|- x
5		cvv	|- _V
6		vy	|- y
7	4	cv	|- x
8		cadds	|- +s
9		c1s	|- 1s
10	7 9 8	co	|- ( x +s 1s )
11	6	cv	|- y
12	10 2	cfv	|- ( F ` ( x +s 1s ) )
13	11 12 1	co	|- ( y .+ ( F ` ( x +s 1s ) ) )
14	10 13	cop	|- <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >.
15	4 6 5 5 14	cmpo	|- ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. )
16	0 2	cfv	|- ( F ` M )
17	0 16	cop	|- <. M , ( F ` M ) >.
18	15 17	crdg	|- rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. )
19		com	|- _om
20	18 19	cima	|- ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )
21	3 20	wceq	|- seq_s M ( .+ , F ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( y .+ ( F ` ( x +s 1s ) ) ) >. ) , <. M , ( F ` M ) >. ) " _om )