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 \in On \to A ↑_{𝑜} 1_{𝑜} = A$

Step	Hyp	Ref	Expression
1		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
2	1	oveq2i	$⊢ A ↑_{𝑜} 1_{𝑜} = A ↑_{𝑜} suc \emptyset$
3		peano1	$⊢ \emptyset \in ω$
4		onesuc	$⊢ (A \in On \land \emptyset \in ω) \to A ↑_{𝑜} suc \emptyset = (A ↑_{𝑜} \emptyset) \cdot_{𝑜} A$
5	3 4	mpan2	$⊢ A \in On \to A ↑_{𝑜} suc \emptyset = (A ↑_{𝑜} \emptyset) \cdot_{𝑜} A$
6	2 5	eqtrid	$⊢ A \in On \to A ↑_{𝑜} 1_{𝑜} = (A ↑_{𝑜} \emptyset) \cdot_{𝑜} A$
7		oe0	$⊢ A \in On \to A ↑_{𝑜} \emptyset = 1_{𝑜}$
8	7	oveq1d	$⊢ A \in On \to (A ↑_{𝑜} \emptyset) \cdot_{𝑜} A = 1_{𝑜} \cdot_{𝑜} A$
9		om1r	$⊢ A \in On \to 1_{𝑜} \cdot_{𝑜} A = A$
10	6 8 9	3eqtrd	$⊢ A \in On \to A ↑_{𝑜} 1_{𝑜} = A$

Metamath Proof Explorer