Theorem nmulfn

Description: Natural multiplication is a function over pairs of ordinals. (Contributed by Scott Fenton, 2-Jun-2026)

	Ref	Expression
Assertion	nmulfn	⊢ ·no Fn ( On × On )

Proof

Step	Hyp	Ref	Expression
1		df-nmul	⊢ ·no = frecs ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ∧ ( ( ( 1st ‘ 𝑥 ) E ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) E ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) } , ( On × On ) , ( 𝑝 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑝 ) / 𝑎 ⦌ ⦋ ( 2nd ‘ 𝑝 ) / 𝑏 ⦌ ∩ { 𝑧 ∈ On ∣ ∀ 𝑐 ∈ 𝑎 ∀ 𝑑 ∈ 𝑏 ( ( 𝑐 𝑚 𝑏 ) +no ( 𝑎 𝑚 𝑑 ) ) ∈ ( 𝑧 +no ( 𝑐 𝑚 𝑑 ) ) } ) )
2	1	on2recsfn	⊢ ·no Fn ( On × On )