Theorem fnom

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

	Ref	Expression
Assertion	fnom	⊢ ·o Fn ( On × On )

Proof

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