Theorem nnexpscl

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

	Ref	Expression
Assertion	nnexpscl	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ ℕs )

Proof

Step	Hyp	Ref	Expression
1		nnssno	⊢ ℕs ⊆ No
2		nnmulscl	⊢ ( ( 𝑥 ∈ ℕs ∧ 𝑦 ∈ ℕs ) → ( 𝑥 ·s 𝑦 ) ∈ ℕs )
3		1nns	⊢ 1s ∈ ℕs
4	1 2 3	expscllem	⊢ ( ( 𝐴 ∈ ℕs ∧ 𝑁 ∈ ℕ0s ) → ( 𝐴 ↑s 𝑁 ) ∈ ℕs )