df-oadd

Description: Define the ordinal addition operation. (Contributed by NM, 3-May-1995)

		Ref	Expression
	Assertion	df-oadd	$⊢ +_{𝑜} = (x \in On, y \in On ⟼ rec ((z \in V ⟼ suc z), x) (y))$

Step	Hyp	Ref	Expression
0		coa	$class +_{𝑜}$
1		vx	$setvar x$
2		con0	$class On$
3		vy	$setvar y$
4		vz	$setvar z$
5		cvv	$class V$
6	4	cv	$setvar z$
7	6	csuc	$class suc z$
8	4 5 7	cmpt	$class (z \in V ⟼ suc z)$
9	1	cv	$setvar x$
10	8 9	crdg	$class rec ((z \in V ⟼ suc z), x)$
11	3	cv	$setvar y$
12	11 10	cfv	$class rec ((z \in V ⟼ suc z), x) (y)$
13	1 3 2 2 12	cmpo	$class (x \in On, y \in On ⟼ rec ((z \in V ⟼ suc z), x) (y))$
14	0 13	wceq	$wff +_{𝑜} = (x \in On, y \in On ⟼ rec ((z \in V ⟼ suc z), x) (y))$

Metamath Proof Explorer