Theorem noseqno

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

	Ref	Expression
Hypotheses	noseq.1	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
	noseq.2	|- ( ph -> A e. No )
	noseqno.3	|- ( ph -> B e. Z )
Assertion	noseqno	|- ( ph -> B e. No )

Proof

Step	Hyp	Ref	Expression
1		noseq.1	|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , A ) " _om ) )
2		noseq.2	|- ( ph -> A e. No )
3		noseqno.3	|- ( ph -> B e. Z )
4	1 2	noseqssno	|- ( ph -> Z C_ No )
5	4 3	sseldd	|- ( ph -> B e. No )