Theorem absscl

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

	Ref	Expression
Assertion	absscl	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) ∈ No )

Proof

Step	Hyp	Ref	Expression
1		abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
2		id	⊢ ( 𝐴 ∈ No → 𝐴 ∈ No )
3		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
4	2 3	ifcld	⊢ ( 𝐴 ∈ No → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) ∈ No )
5	1 4	eqeltrd	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) ∈ No )