Metamath Proof Explorer

Theorem abssor

Description: The absolute value of a surreal is either that surreal or its negative. (Contributed by Scott Fenton, 16-Apr-2025)

Ref Expression
Assertion abssor 
|- ( A e. No -> ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) )

Proof

Step Hyp Ref Expression
1 ifeqor 
 |-  ( if ( 0s <_s A , A , ( -us ` A ) ) = A \/ if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) )
2 abssval 
 |-  ( A e. No -> ( abs_s ` A ) = if ( 0s <_s A , A , ( -us ` A ) ) )
3 2 eqeq1d 
 |-  ( A e. No -> ( ( abs_s ` A ) = A <-> if ( 0s <_s A , A , ( -us ` A ) ) = A ) )
4 2 eqeq1d 
 |-  ( A e. No -> ( ( abs_s ` A ) = ( -us ` A ) <-> if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) ) )
5 3 4 orbi12d 
 |-  ( A e. No -> ( ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) <-> ( if ( 0s <_s A , A , ( -us ` A ) ) = A \/ if ( 0s <_s A , A , ( -us ` A ) ) = ( -us ` A ) ) ) )
6 1 5 mpbiri 
 |-  ( A e. No -> ( ( abs_s ` A ) = A \/ ( abs_s ` A ) = ( -us ` A ) ) )