Theorem seqsfn

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

	Ref	Expression
Hypotheses	seqsfn.1	⊢ ( 𝜑 → 𝑀 ∈ No )
	seqsfn.2	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) )
Assertion	seqsfn	⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) Fn 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		seqsfn.1	⊢ ( 𝜑 → 𝑀 ∈ No )
2		seqsfn.2	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) )
3		eqidd	⊢ ( 𝜑 → ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) ↾ ω ) )
4		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 +s 1s ) = ( 𝑦 +s 1s ) )
5	4	cbvmptv	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) = ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) )
6		rdgeq1	⊢ ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) = ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) → rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) = rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) )
7	5 6	ax-mp	⊢ rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) = rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 )
8	7	imaeq1i	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) “ ω )
9	2 8	eqtrdi	⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑦 ∈ V ↦ ( 𝑦 +s 1s ) ) , 𝑀 ) “ ω ) )
10		fvexd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ V )
11		eqidd	⊢ ( 𝜑 → ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
12	11	seqsval	⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = ran ( rec ( ( 𝑦 ∈ V , 𝑧 ∈ V ↦ ⟨ ( 𝑦 +s 1s ) , ( 𝑦 ( 𝑤 ∈ V , 𝑡 ∈ V ↦ ( 𝑡 + ( 𝐹 ‘ ( 𝑤 +s 1s ) ) ) ) 𝑧 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
13	1 3 9 10 11 12	noseqrdgfn	⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) Fn 𝑍 )