Definition df-oadd

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

	Ref	Expression
Assertion	df-oadd	⊢ +o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		coa	⊢ +o
1		vx	⊢ 𝑥
2		con0	⊢ On
3		vy	⊢ 𝑦
4		vz	⊢ 𝑧
5		cvv	⊢ V
6	4	cv	⊢ 𝑧
7	6	csuc	⊢ suc 𝑧
8	4 5 7	cmpt	⊢ ( 𝑧 ∈ V ↦ suc 𝑧 )
9	1	cv	⊢ 𝑥
10	8 9	crdg	⊢ rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 )
11	3	cv	⊢ 𝑦
12	11 10	cfv	⊢ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 )
13	1 3 2 2 12	cmpo	⊢ ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 ) )
14	0 13	wceq	⊢ +o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 ) )