Metamath Proof Explorer

Theorem exps1

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

Ref Expression
Assertion exps1 
|- ( A e. No -> ( A ^su 1s ) = A )

Proof

Step Hyp Ref Expression
1 1nns 
 |-  1s e. NN_s
2 expsnnval 
 |-  ( ( A e. No /\ 1s e. NN_s ) -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) )
3 1 2 mpan2 
 |-  ( A e. No -> ( A ^su 1s ) = ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) )
4 1sno 
 |-  1s e. No
5 4 a1i 
 |-  ( A e. No -> 1s e. No )
6 5 seqs1 
 |-  ( A e. No -> ( seq_s 1s ( x.s , ( NN_s X. { A } ) ) ` 1s ) = ( ( NN_s X. { A } ) ` 1s ) )
7 fvconst2g 
 |-  ( ( A e. No /\ 1s e. NN_s ) -> ( ( NN_s X. { A } ) ` 1s ) = A )
8 1 7 mpan2 
 |-  ( A e. No -> ( ( NN_s X. { A } ) ` 1s ) = A )
9 3 6 8 3eqtrd 
 |-  ( A e. No -> ( A ^su 1s ) = A )