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	⊢ ( 𝐴 ∈ No → ( ( abss ‘ 𝐴 ) = 𝐴 ∨ ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ifeqor	⊢ ( if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = 𝐴 ∨ if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) )
2		abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
3	2	eqeq1d	⊢ ( 𝐴 ∈ No → ( ( abss ‘ 𝐴 ) = 𝐴 ↔ if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = 𝐴 ) )
4	2	eqeq1d	⊢ ( 𝐴 ∈ No → ( ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ↔ if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) ) )
5	3 4	orbi12d	⊢ ( 𝐴 ∈ No → ( ( ( abss ‘ 𝐴 ) = 𝐴 ∨ ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) ↔ ( if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = 𝐴 ∨ if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) = ( -us ‘ 𝐴 ) ) ) )
6	1 5	mpbiri	⊢ ( 𝐴 ∈ No → ( ( abss ‘ 𝐴 ) = 𝐴 ∨ ( abss ‘ 𝐴 ) = ( -us ‘ 𝐴 ) ) )