Theorem seqsfn

Description: The surreal sequence builder is a function. (Contributed by Scott Fenton, 19-Apr-2025)

	Ref	Expression
Hypotheses	seqsfn.1	|- ( ph -> M e. No )
	seqsfn.2	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) )
Assertion	seqsfn	|- ( ph -> seq_s M ( .+ , F ) Fn Z )

Proof

Step	Hyp	Ref	Expression
1		seqsfn.1	|- ( ph -> M e. No )
2		seqsfn.2	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) )
3		eqidd	|- ( ph -> ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) |` _om ) = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) |` _om ) )
4		oveq1	|- ( x = y -> ( x +s 1s ) = ( y +s 1s ) )
5	4	cbvmptv	|- ( x e. _V |-> ( x +s 1s ) ) = ( y e. _V |-> ( y +s 1s ) )
6		rdgeq1	|- ( ( x e. _V |-> ( x +s 1s ) ) = ( y e. _V |-> ( y +s 1s ) ) -> rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) = rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) )
7	5 6	ax-mp	|- rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) = rec ( ( y e. _V |-> ( y +s 1s ) ) , M )
8	7	imaeq1i	|- ( rec ( ( x e. _V |-> ( x +s 1s ) ) , M ) " _om ) = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) " _om )
9	2 8	eqtrdi	|- ( ph -> Z = ( rec ( ( y e. _V |-> ( y +s 1s ) ) , M ) " _om ) )
10		fvexd	|- ( ph -> ( F ` M ) e. _V )
11		eqidd	|- ( ph -> ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) = ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
12	11	seqsval	|- ( ph -> seq_s M ( .+ , F ) = ran ( rec ( ( y e. _V , z e. _V |-> <. ( y +s 1s ) , ( y ( w e. _V , t e. _V |-> ( t .+ ( F ` ( w +s 1s ) ) ) ) z ) >. ) , <. M , ( F ` M ) >. ) |` _om ) )
13	1 3 9 10 11 12	noseqrdgfn	|- ( ph -> seq_s M ( .+ , F ) Fn Z )