Theorem exps1

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

	Ref	Expression
Assertion	exps1	Could not format assertion : No typesetting found for |- ( A e. No -> ( A ^su 1s ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		1nns	$$⊢1_s\in {\mathbb{N}}_s$$
2		expsnnval	Could not format ( ( A e. No /\ 1s e. NN_s ) -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) ) : No typesetting found for |- ( ( A e. No /\ 1s e. NN_s ) -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) ) with typecode |-
3	1 2	mpan2	Could not format ( A e. No -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) ) : No typesetting found for |- ( A e. No -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) ) with typecode |-
4		1sno	$$⊢1_s\in \mathrm{No}$$
5	4	a1i	$$⊢A\in \mathrm{No}\to 1_s\in \mathrm{No}$$
6	5	seqs1	$$⊢A\in \mathrm{No}\to {seq}_s{1}_s\left({\cdot }_s,\left({\mathbb{N}}_s\times \left\{A\right\}\right)\right)\left(1_s\right)=\left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(1_s\right)$$
7		fvconst2g	$$⊢\left(A\in \mathrm{No}\wedge 1_s\in {\mathbb{N}}_s\right)\to \left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(1_s\right)=A$$
8	1 7	mpan2	$$⊢A\in \mathrm{No}\to \left({\mathbb{N}}_s\times \left\{A\right\}\right)\left(1_s\right)=A$$
9	3 6 8	3eqtrd	Could not format ( A e. No -> ( A ^su 1s ) = A ) : No typesetting found for |- ( A e. No -> ( A ^su 1s ) = A ) with typecode |-