Theorem noseqno

Description: An element of a surreal sequence is a surreal. (Contributed by Scott Fenton, 18-Apr-2025)

	Ref	Expression
Hypotheses	noseq.1	$$⊢\phi \to Z=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),A\right)\left[\mathrm{\omega }\right]$$
	noseq.2	$$⊢\phi \to A\in \mathrm{No}$$
	noseqno.3	$$⊢\phi \to B\in Z$$
Assertion	noseqno	$$⊢\phi \to B\in \mathrm{No}$$

Proof

Step	Hyp	Ref	Expression
1		noseq.1	$$⊢\phi \to Z=\mathrm{rec}\left(\left(x\in \mathrm{V}⟼x{+}_s{1}_s\right),A\right)\left[\mathrm{\omega }\right]$$
2		noseq.2	$$⊢\phi \to A\in \mathrm{No}$$
3		noseqno.3	$$⊢\phi \to B\in Z$$
4	1 2	noseqssno	$$⊢\phi \to Z\subseteq \mathrm{No}$$
5	4 3	sseldd	$$⊢\phi \to B\in \mathrm{No}$$