Metamath Proof Explorer

Theorem absscl

Description: Closure law for surreal absolute value. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion absscl 
|- ( A e. No -> ( abs_s ` A ) e. No )

Proof

Step Hyp Ref Expression
1 abssval 
 |-  ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )
2 id 
 |-  ( A e. No -> A e. No )
3 negscl 
 |-  ( A e. No -> ( -us ` A ) e. No )
4 2 3 ifcld 
 |-  ( A e. No -> if ( 0s <_s A , A , ( -us ` A ) ) e. No )
5 1 4 eqeltrd 
 |-  ( A e. No -> ( abs_s ` A ) e. No )