Theorem seqsex

Description: Existence of the surreal sequence builder operation. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Assertion	seqsex	⊢ seqs 𝑀 ( + , 𝐹 ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-seqs	⊢ seqs 𝑀 ( + , 𝐹 ) = ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω )
2		rdgfun	⊢ Fun rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ )
3		dcomex	⊢ ω ∈ V
4	3	funimaex	⊢ ( Fun rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) → ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) ∈ V )
5	2 4	ax-mp	⊢ ( rec ( ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ⟨ ( 𝑥 +s 1s ) , ( 𝑦 + ( 𝐹 ‘ ( 𝑥 +s 1s ) ) ) ⟩ ) , ⟨ 𝑀 , ( 𝐹 ‘ 𝑀 ) ⟩ ) “ ω ) ∈ V
6	1 5	eqeltri	⊢ seqs 𝑀 ( + , 𝐹 ) ∈ V