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 (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	$class M$
1		c.pl	$class \underset{˙}{+}$
2		cF	$class F$
3	1 2 0	cseqs	$class {seq}_{s} M (\underset{˙}{+}, F)$
4		vx	$setvar x$
5		cvv	$class V$
6		vy	$setvar y$
7	4	cv	$setvar x$
8		cadds	$class +_{s}$
9		c1s	$class 1_{s}$
10	7 9 8	co	$class (x +_{s} 1_{s})$
11	6	cv	$setvar y$
12	10 2	cfv	$class F (x +_{s} 1_{s})$
13	11 12 1	co	$class (y \underset{˙}{+} F (x +_{s} 1_{s}))$
14	10 13	cop	$class ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩$
15	4 6 5 5 14	cmpo	$class (x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩)$
16	0 2	cfv	$class F (M)$
17	0 16	cop	$class ⟨M, F (M)⟩$
18	15 17	crdg	$class rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩)$
19		com	$class ω$
20	18 19	cima	$class rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$
21	3 20	wceq	$wff {seq}_{s} M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$

Metamath Proof Explorer

Definition df-seqs

Detailed syntax breakdown