Theorem 1sno

Description: Surreal one is a surreal. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	1sno	|- 1s e. No

Proof

Step	Hyp	Ref	Expression
1		df-1s	|- 1s = ( { 0s } |s (/) )
2		0sno	|- 0s e. No
3		snelpwi	|- ( 0s e. No -> { 0s } e. ~P No )
4	2 3	ax-mp	|- { 0s } e. ~P No
5		nulssgt	|- ( { 0s } e. ~P No -> { 0s } <
6	4 5	ax-mp	|- { 0s } <
7		scutcl	|- ( { 0s } < ( { 0s } |s (/) ) e. No )
8	6 7	ax-mp	|- ( { 0s } |s (/) ) e. No
9	1 8	eqeltri	|- 1s e. No