Theorem seqn0sfn

Description: The surreal sequence builder is a function over NN0_s when started from zero. (Contributed by Scott Fenton, 19-Apr-2025)

	Ref	Expression
Assertion	seqn0sfn	$$⊢\phi \to {seq}_s{0}_s\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{N}}_{\mathrm{0s}}$$

Proof

Step	Hyp	Ref	Expression
1		0sno	$$⊢0_s\in \mathrm{No}$$
2	1	a1i	$$⊢\phi \to 0_s\in \mathrm{No}$$
3		df-n0s	$$⊢{\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$
4	3	a1i	$$⊢\phi \to {\mathbb{N}}_{\mathrm{0s}}=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),0_s\right)\left[\mathrm{\omega }\right]$$
5	2 4	seqsfn	$$⊢\phi \to {seq}_s{0}_s\left(\underset{\dot{}}{+},F\right)Fn{\mathbb{N}}_{\mathrm{0s}}$$