Theorem 0no

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

	Ref	Expression
Assertion	0no	⊢ 0s ∈ No

Proof

Step	Hyp	Ref	Expression
1		df-0s	⊢ 0s = ( ∅ |s ∅ )
2		0elpw	⊢ ∅ ∈ 𝒫 No
3		nulsgts	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
4	2 3	ax-mp	⊢ ∅ <<s ∅
5		cutscl	⊢ ( ∅ <<s ∅ → ( ∅ |s ∅ ) ∈ No )
6	4 5	ax-mp	⊢ ( ∅ |s ∅ ) ∈ No
7	1 6	eqeltri	⊢ 0s ∈ No