Theorem noseqssno

Description: A surreal sequence is a subset of the surreals. (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 )
Assertion	noseqssno	|- ( ph -> Z C_ 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		peano2no	|- ( y e. No -> ( y +s 1s ) e. No )
4	3	adantl	|- ( ( ph /\ y e. No ) -> ( y +s 1s ) e. No )
5	1 2 2 4	noseqind	|- ( ph -> Z C_ No )