Metamath Proof Explorer

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 + 𝑜 Fn On × On


Step Hyp Ref Expression
1 df-oadd + 𝑜 = x On , y On rec z V suc z x y
2 fvex rec z V suc z x y V
3 1 2 fnmpoi + 𝑜 Fn On × On