This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oe1

Description: Ordinal exponentiation with an exponent of 1. Lemma 2.16 of Schloeder p. 6. (Contributed by NM, 2-Jan-2005)

Ref Expression
Assertion oe1 
|- ( A e. On -> ( A ^o 1o ) = A )

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 1 oveq2i 
 |-  ( A ^o 1o ) = ( A ^o suc (/) )
3 peano1 
 |-  (/) e. _om
4 onesuc 
 |-  ( ( A e. On /\ (/) e. _om ) -> ( A ^o suc (/) ) = ( ( A ^o (/) ) .o A ) )
5 3 4 mpan2 
 |-  ( A e. On -> ( A ^o suc (/) ) = ( ( A ^o (/) ) .o A ) )
6 2 5 eqtrid 
 |-  ( A e. On -> ( A ^o 1o ) = ( ( A ^o (/) ) .o A ) )
7 oe0 
 |-  ( A e. On -> ( A ^o (/) ) = 1o )
8 7 oveq1d 
 |-  ( A e. On -> ( ( A ^o (/) ) .o A ) = ( 1o .o A ) )
9 om1r 
 |-  ( A e. On -> ( 1o .o A ) = A )
10 6 8 9 3eqtrd 
 |-  ( A e. On -> ( A ^o 1o ) = A )