Theorem n0expscl

Description: Closure law for non-negative surreal integer exponentiation. (Contributed by Scott Fenton, 7-Nov-2025)

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

Proof

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