oav

Description: Value of ordinal addition. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

		Ref	Expression
	Assertion	oav	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B = rec ((x \in V ⟼ suc x), A) (B)$

Step	Hyp	Ref	Expression
1		rdgeq2	$⊢ y = A \to rec ((x \in V ⟼ suc x), y) = rec ((x \in V ⟼ suc x), A)$
2	1	fveq1d	$⊢ y = A \to rec ((x \in V ⟼ suc x), y) (z) = rec ((x \in V ⟼ suc x), A) (z)$
3		fveq2	$⊢ z = B \to rec ((x \in V ⟼ suc x), A) (z) = rec ((x \in V ⟼ suc x), A) (B)$
4		df-oadd	$⊢ +_{𝑜} = (y \in On, z \in On ⟼ rec ((x \in V ⟼ suc x), y) (z))$
5		fvex	$⊢ rec ((x \in V ⟼ suc x), A) (B) \in V$
6	2 3 4 5	ovmpo	$⊢ (A \in On \land B \in On) \to A +_{𝑜} B = rec ((x \in V ⟼ suc x), A) (B)$

Metamath Proof Explorer