Theorem 1sne0s

Description: Surreal zero does not equal surreal one. (Contributed by Scott Fenton, 5-Sep-2025)

	Ref	Expression
Assertion	1sne0s	$$⊢1_s\ne 0_s$$

Proof

Step	Hyp	Ref	Expression
1		0slt1s	$$⊢0_s{<}_s{1}_s$$
2		sgt0ne0	$$⊢0_s{<}_s{1}_s\to 1_s\ne 0_s$$
3	1 2	ax-mp	$$⊢1_s\ne 0_s$$