Theorem expscl

Description: Closure law for surreal exponentiation. (Contributed by Scott Fenton, 7-Aug-2025)

	Ref	Expression
Assertion	expscl	|- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su N ) e. No )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- No C_ No
2		mulscl	|- ( ( x e. No /\ y e. No ) -> ( x x.s y ) e. No )
3		1sno	|- 1s e. No
4	1 2 3	expscllem	|- ( ( A e. No /\ N e. NN0_s ) -> ( A ^su N ) e. No )