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	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o 1o ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	oveq2i	⊢ ( 𝐴 ↑o 1o ) = ( 𝐴 ↑o suc ∅ )
3		peano1	⊢ ∅ ∈ ω
4		onesuc	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ω ) → ( 𝐴 ↑o suc ∅ ) = ( ( 𝐴 ↑o ∅ ) ·o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o suc ∅ ) = ( ( 𝐴 ↑o ∅ ) ·o 𝐴 ) )
6	2 5	eqtrid	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o 1o ) = ( ( 𝐴 ↑o ∅ ) ·o 𝐴 ) )
7		oe0	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o ∅ ) = 1o )
8	7	oveq1d	⊢ ( 𝐴 ∈ On → ( ( 𝐴 ↑o ∅ ) ·o 𝐴 ) = ( 1o ·o 𝐴 ) )
9		om1r	⊢ ( 𝐴 ∈ On → ( 1o ·o 𝐴 ) = 𝐴 )
10	6 8 9	3eqtrd	⊢ ( 𝐴 ∈ On → ( 𝐴 ↑o 1o ) = 𝐴 )