Theorem expscl

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

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

Proof

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