Theorem seqs1

Description: The value of the surreal sequence bulder function at its initial value. (Contributed by Scott Fenton, 19-Apr-2025)

	Ref	Expression
Hypothesis	seqs1.1	|- ( ph -> M e. No )
Assertion	seqs1	|- ( ph -> ( seq_s M ( .+ , F ) ` M ) = ( F ` M ) )

Proof

Step	Hyp	Ref	Expression
1		seqs1.1	|- ( ph -> M e. No )
2		eqidd	|- ( ph -> ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) |` _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) |` _om ) )
3		eqidd	|- ( ph -> ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) )
4		fvexd	|- ( ph -> ( F ` M ) e. _V )
5		eqidd	|- ( ph -> ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) = ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
6	5	seqsval	|- ( ph -> seq_s M ( .+ , F ) = ran ( rec ( ( x e. _V , y e. _V |-> <. ( x +s 1s ) , ( x ( z e. _V , w e. _V |-> ( w .+ ( F ` ( z +s 1s ) ) ) ) y ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
7	1 2 3 4 5 6	noseqrdg0	|- ( ph -> ( seq_s M ( .+ , F ) ` M ) = ( F ` M ) )