Metamath Proof Explorer

Theorem noseqex

Description: The next several theorems develop the concept of a countable sequence of surreals. This set is denoted by Z here and is the analogue of the upper integer sets for surreal numbers. However, we do not require the starting point to be an integer so we can accommodate infinite numbers. This first theorem establishes that Z is a set. (Contributed by Scott Fenton, 18-Apr-2025)

		Ref	Expression
	Hypothesis	noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
	Assertion	noseqex	$⊢ φ \to Z \in V$

Proof

Step	Hyp	Ref	Expression
1		noseq.1	$⊢ φ \to Z = rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω]$
2		rdgfun	$⊢ Fun rec ((x \in V ⟼ x +_{s} 1_{s}), A)$
3		dcomex	$⊢ ω \in V$
4	3	funimaex	$⊢ Fun rec ((x \in V ⟼ x +_{s} 1_{s}), A) \to rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω] \in V$
5	2 4	ax-mp	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), A) [ω] \in V$
6	1 5	eqeltrdi	$⊢ φ \to Z \in V$