Theorem oav

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

	Ref	Expression
Assertion	oav	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rdgeq2	⊢ ( 𝑦 = 𝐴 → rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) = rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) )
2	1	fveq1d	⊢ ( 𝑦 = 𝐴 → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝑧 ) )
3		fveq2	⊢ ( 𝑧 = 𝐵 → ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝑧 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )
4		df-oadd	⊢ +o = ( 𝑦 ∈ On , 𝑧 ∈ On ↦ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝑦 ) ‘ 𝑧 ) )
5		fvex	⊢ ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) ∈ V
6	2 3 4 5	ovmpo	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 +o 𝐵 ) = ( rec ( ( 𝑥 ∈ V ↦ suc 𝑥 ) , 𝐴 ) ‘ 𝐵 ) )