Theorem n0ons

Description: A surreal natural is a surreal ordinal. (Contributed by Scott Fenton, 2-Apr-2025)

	Ref	Expression
Assertion	n0ons	|- ( A e. NN0_s -> A e. On_s )

Proof

Step	Hyp	Ref	Expression
1		n0sno	|- ( A e. NN0_s -> A e. No )
2		1sno	|- 1s e. No
3		subscl	|- ( ( A e. No /\ 1s e. No ) -> ( A -s 1s ) e. No )
4	1 2 3	sylancl	|- ( A e. NN0_s -> ( A -s 1s ) e. No )
5		ovex	|- ( A -s 1s ) e. _V
6	5	snelpw	|- ( ( A -s 1s ) e. No <-> { ( A -s 1s ) } e. ~P No )
7	4 6	sylib	|- ( A e. NN0_s -> { ( A -s 1s ) } e. ~P No )
8		n0scut	|- ( A e. NN0_s -> A = ( { ( A -s 1s ) } |s (/) ) )
9		oveq1	|- ( x = { ( A -s 1s ) } -> ( x |s (/) ) = ( { ( A -s 1s ) } |s (/) ) )
10	9	eqeq2d	|- ( x = { ( A -s 1s ) } -> ( A = ( x |s (/) ) <-> A = ( { ( A -s 1s ) } |s (/) ) ) )
11	10	rspcev	|- ( ( { ( A -s 1s ) } e. ~P No /\ A = ( { ( A -s 1s ) } |s (/) ) ) -> E. x e. ~P No A = ( x |s (/) ) )
12	7 8 11	syl2anc	|- ( A e. NN0_s -> E. x e. ~P No A = ( x |s (/) ) )
13		elons2	|- ( A e. On_s <-> E. x e. ~P No A = ( x |s (/) ) )
14	12 13	sylibr	|- ( A e. NN0_s -> A e. On_s )