oe2

		Ref	Expression
	Assertion	oe2	$⊢ A \in On \to A \cdot_{𝑜} A = A ↑_{𝑜} 2_{𝑜}$

Step	Hyp	Ref	Expression
1		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
2	1	oveq2i	$⊢ A ↑_{𝑜} 2_{𝑜} = A ↑_{𝑜} suc 1_{𝑜}$
3		1on	$⊢ 1_{𝑜} \in On$
4		oesuc	$⊢ (A \in On \land 1_{𝑜} \in On) \to A ↑_{𝑜} suc 1_{𝑜} = (A ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} A$
5	3 4	mpan2	$⊢ A \in On \to A ↑_{𝑜} suc 1_{𝑜} = (A ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} A$
6		oe1	$⊢ A \in On \to A ↑_{𝑜} 1_{𝑜} = A$
7	6	oveq1d	$⊢ A \in On \to (A ↑_{𝑜} 1_{𝑜}) \cdot_{𝑜} A = A \cdot_{𝑜} A$
8	5 7	eqtrd	$⊢ A \in On \to A ↑_{𝑜} suc 1_{𝑜} = A \cdot_{𝑜} A$
9	2 8	eqtr2id	$⊢ A \in On \to A \cdot_{𝑜} A = A ↑_{𝑜} 2_{𝑜}$

Metamath Proof Explorer