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	⊢ ( 𝜑 → 𝑀 ∈ No )
Assertion	seqs1	⊢ ( 𝜑 → ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		seqs1.1	⊢ ( 𝜑 → 𝑀 ∈ No )
2		eqidd	⊢ ( 𝜑 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) ↾ ω ) )
3		eqidd	⊢ ( 𝜑 → ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝑀 ) “ ω ) )
4		fvexd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑀 ) ∈ V )
5		eqidd	⊢ ( 𝜑 → ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
6	5	seqsval	⊢ ( 𝜑 → seqs 𝑀 ( + , 𝐹 ) = ran ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑥 ( 𝑧 ∈ V , 𝑤 ∈ V ↦ ( 𝑤 + ( 𝐹 ‘ ( 𝑧 +s 1s ) ) ) ) 𝑦 ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) ↾ ω ) )
7	1 2 3 4 5 6	noseqrdg0	⊢ ( 𝜑 → ( seqs 𝑀 ( + , 𝐹 ) ‘ 𝑀 ) = ( 𝐹 ‘ 𝑀 ) )