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	⊢ ( 𝜑 → seqs 0s ( + , 𝐹 ) Fn ℕ0s )

Proof

Step	Hyp	Ref	Expression
1		0sno	⊢ 0s ∈ No
2	1	a1i	⊢ ( 𝜑 → 0s ∈ No )
3		df-n0s	⊢ ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω )
4	3	a1i	⊢ ( 𝜑 → ℕ0s = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 0s ) “ ω ) )
5	2 4	seqsfn	⊢ ( 𝜑 → seqs 0s ( + , 𝐹 ) Fn ℕ0s )