Theorem nmulr0

Description: Natural multiplication by zero. (Contributed by Scott Fenton, 10-Jun-2026)

	Ref	Expression
Assertion	nmulr0	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		0elon	⊢ ∅ ∈ On
2		nmulval	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ·no ∅ ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } )
3	1 2	mpan2	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no ∅ ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } )
4		ral0	⊢ ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) )
5	4	rgenw	⊢ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) )
6		oveq1	⊢ ( 𝑥 = ∅ → ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) = ( ∅ +no ( 𝑎 ·no 𝑏 ) ) )
7	6	eleq2d	⊢ ( 𝑥 = ∅ → ( ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) ) ) )
8	7	2ralbidv	⊢ ( 𝑥 = ∅ → ( ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) ) ) )
9	8	elrab3	⊢ ( ∅ ∈ On → ( ∅ ∈ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) ) ) )
10	1 9	ax-mp	⊢ ( ∅ ∈ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } ↔ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( ∅ +no ( 𝑎 ·no 𝑏 ) ) )
11	5 10	mpbir	⊢ ∅ ∈ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) }
12		int0el	⊢ ( ∅ ∈ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } → ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∅ )
13	11 12	ax-mp	⊢ ∩ { 𝑥 ∈ On ∣ ∀ 𝑎 ∈ 𝐴 ∀ 𝑏 ∈ ∅ ( ( 𝑎 ·no ∅ ) +no ( 𝐴 ·no 𝑏 ) ) ∈ ( 𝑥 +no ( 𝑎 ·no 𝑏 ) ) } = ∅
14	3 13	eqtrdi	⊢ ( 𝐴 ∈ On → ( 𝐴 ·no ∅ ) = ∅ )