Theorem nmulval

Description: Show the value of natural multiplication. (Contributed by Scott Fenton, 10-Jun-2026)

	Ref	Expression
Assertion	nmulval	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		nmulprop	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ·no 𝐵 ) ∈ On ∧ ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ) )
2	1	simprd	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ·no 𝐵 ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ·no 𝐵 ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } )