Theorem nnexpscl

Description: Closure law for positive surreal integer exponentiation. (Contributed by Scott Fenton, 8-Nov-2025)

	Ref	Expression
Assertion	nnexpscl	Could not format assertion : No typesetting found for |- ( ( A e. NN_s /\ N e. NN0_s ) -> ( A ^su N ) e. NN_s ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		nnssno	$$⊢{\mathbb{N}}_s\subseteq \mathrm{No}$$
2		nnmulscl	$$⊢\left(x\in {\mathbb{N}}_s\wedge y\in {\mathbb{N}}_s\right)\to x{\cdot }_{s}y\in {\mathbb{N}}_s$$
3		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
4	1 2 3	expscllem	Could not format ( ( A e. NN_s /\ N e. NN0_s ) -> ( A ^su N ) e. NN_s ) : No typesetting found for |- ( ( A e. NN_s /\ N e. NN0_s ) -> ( A ^su N ) e. NN_s ) with typecode |-