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 )