seqsex

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

		Ref	Expression
	Assertion	seqsex	$⊢ {seq}_{s} M (\underset{˙}{+}, F) \in V$

Step	Hyp	Ref	Expression
1		df-seqs	$⊢ {seq}_{s} M (\underset{˙}{+}, F) = rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω]$
2		rdgfun	$⊢ Fun rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩)$
3		dcomex	$⊢ ω \in V$
4	3	funimaex	$⊢ Fun rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) \to rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω] \in V$
5	2 4	ax-mp	$⊢ rec ((x \in V, y \in V ⟼ ⟨x +_{s} 1_{s}, y \underset{˙}{+} F (x +_{s} 1_{s})⟩), ⟨M, F (M)⟩) [ω] \in V$
6	1 5	eqeltri	$⊢ {seq}_{s} M (\underset{˙}{+}, F) \in V$

Metamath Proof Explorer