Metamath Proof Explorer

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 
|- ( ph -> seq_s 0s ( .+ , F ) Fn NN0_s )

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 1 a1i 
 |-  ( ph -> 0s e. No )
3 df-n0s 
 |-  NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om )
4 3 a1i 
 |-  ( ph -> NN0_s = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , 0s ) " _om ) )
5 2 4 seqsfn 
 |-  ( ph -> seq_s 0s ( .+ , F ) Fn NN0_s )