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	⊢ seqs 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	⊢ 𝑀
1		c.pl	⊢ +
2		cF	⊢ 𝐹
3	1 2 0	cseqs	⊢ seqs 𝑀 ( + , 𝐹 )
4		vx	⊢ 𝑥
5		cvv	⊢ V
6		vy	⊢ 𝑦
7	4	cv	⊢ 𝑥
8		cadds	⊢ +s
9		c1s	⊢ 1s
10	7 9 8	co	⊢ ( 𝑥 +s 1s )
11	6	cv	⊢ 𝑦
12	10 2	cfv	⊢ ( 𝐹 ‘ ( 𝑥 +s 1s ) )
13	11 12 1	co	⊢ ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) )
14	10 13	cop	⊢ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩
15	4 6 5 5 14	cmpo	⊢ ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ )
16	0 2	cfv	⊢ ( 𝐹 ‘ 𝑀 )
17	0 16	cop	⊢ ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩
18	15 17	crdg	⊢ rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ )
19		com	⊢ ω
20	18 19	cima	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
21	3 20	wceq	⊢ seqs 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )