Metamath Proof Explorer

Theorem abs0s

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

Ref Expression
Assertion abs0s 
|- ( abs_s ` 0s ) = 0s

Proof

Step Hyp Ref Expression
1 0sno 
 |-  0s e. No
2 slerflex 
 |-  ( 0s e. No -> 0s <_s 0s )
3 1 2 ax-mp 
 |-  0s <_s 0s
4 abssid 
 |-  ( ( 0s e. No /\ 0s <_s 0s ) -> ( abs_s ` 0s ) = 0s )
5 1 3 4 mp2an 
 |-  ( abs_s ` 0s ) = 0s