om2

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

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

Metamath Proof Explorer