Theorem 1sno

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

	Ref	Expression
Assertion	1sno	⊢ 1s ∈ No

Proof

Step	Hyp	Ref	Expression
1		df-1s	⊢ 1s = ( { 0s } |s ∅ )
2		0sno	⊢ 0s ∈ No
3		snelpwi	⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
4	2 3	ax-mp	⊢ { 0s } ∈ 𝒫 No
5		nulssgt	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
6	4 5	ax-mp	⊢ { 0s } <<s ∅
7		scutcl	⊢ ( { 0s } <<s ∅ → ( { 0s } |s ∅ ) ∈ No )
8	6 7	ax-mp	⊢ ( { 0s } |s ∅ ) ∈ No
9	1 8	eqeltri	⊢ 1s ∈ No