Theorem n0expscl

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

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

Proof

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