Theorem exps1

Description: Surreal exponentiation to one. (Contributed by Scott Fenton, 24-Jul-2025)

	Ref	Expression
Assertion	exps1	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 1s ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		1nns	⊢ 1s ∈ ℕs
2		expnnsval	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ ℕs ) → ( 𝐴 ↑s 1s ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 1s ) )
3	1 2	mpan2	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 1s ) = ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 1s ) )
4		1no	⊢ 1s ∈ No
5	4	a1i	⊢ ( 𝐴 ∈ No → 1s ∈ No )
6	5	seqs1	⊢ ( 𝐴 ∈ No → ( seqs 1s ( ·s , ( ℕs × { 𝐴 } ) ) ‘ 1s ) = ( ( ℕs × { 𝐴 } ) ‘ 1s ) )
7		fvconst2g	⊢ ( ( 𝐴 ∈ No ∧ 1s ∈ ℕs ) → ( ( ℕs × { 𝐴 } ) ‘ 1s ) = 𝐴 )
8	1 7	mpan2	⊢ ( 𝐴 ∈ No → ( ( ℕs × { 𝐴 } ) ‘ 1s ) = 𝐴 )
9	3 6 8	3eqtrd	⊢ ( 𝐴 ∈ No → ( 𝐴 ↑s 1s ) = 𝐴 )