Theorem abs0s

Description: The absolute value of surreal zero. (Contributed by Scott Fenton, 16-Apr-2025)

	Ref	Expression
Assertion	abs0s	⊢ ( abss ‘ 0s ) = 0s

Proof

Step	Hyp	Ref	Expression
1		0no	⊢ 0s ∈ No
2		lesid	⊢ ( 0s ∈ No → 0s ≤s 0s )
3	1 2	ax-mp	⊢ 0s ≤s 0s
4		abssid	⊢ ( ( 0s ∈ No ∧ 0s ≤s 0s ) → ( abss ‘ 0s ) = 0s )
5	1 3 4	mp2an	⊢ ( abss ‘ 0s ) = 0s