Theorem fnoa

Description: Functionality and domain of ordinal addition. (Contributed by NM, 26-Aug-1995) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	fnoa	⊢ +o Fn ( On × On )

Proof

Step	Hyp	Ref	Expression
1		df-oadd	⊢ +o = ( 𝑥 ∈ On , 𝑦 ∈ On ↦ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 ) )
2		fvex	⊢ ( rec ( ( 𝑧 ∈ V ↦ suc 𝑧 ) , 𝑥 ) ‘ 𝑦 ) ∈ V
3	1 2	fnmpoi	⊢ +o Fn ( On × On )