Theorem abssval

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

	Ref	Expression
Assertion	abssval	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-abss	⊢ abss = ( 𝑥 ∈ No ↦ if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) ) )
2		breq2	⊢ ( 𝑥 = 𝐴 → ( 0s ≤s 𝑥 ↔ 0s ≤s 𝐴 ) )
3		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
4		fveq2	⊢ ( 𝑥 = 𝐴 → ( -us ‘ 𝑥 ) = ( -us ‘ 𝐴 ) )
5	2 3 4	ifbieq12d	⊢ ( 𝑥 = 𝐴 → if ( 0s ≤s 𝑥 , 𝑥 , ( -us ‘ 𝑥 ) ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )
6		id	⊢ ( 𝐴 ∈ No → 𝐴 ∈ No )
7		negscl	⊢ ( 𝐴 ∈ No → ( -us ‘ 𝐴 ) ∈ No )
8	6 7	ifcld	⊢ ( 𝐴 ∈ No → if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) ∈ No )
9	1 5 6 8	fvmptd3	⊢ ( 𝐴 ∈ No → ( abss ‘ 𝐴 ) = if ( 0s ≤s 𝐴 , 𝐴 , ( -us ‘ 𝐴 ) ) )