Theorem om0r

Description: Ordinal multiplication with zero. Proposition 8.18(1) of TakeutiZaring p. 63. (Contributed by NM, 3-Aug-2004)

	Ref	Expression
Assertion	om0r	⊢ ( 𝐴 ∈ On → ( ∅ ·o 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = ∅ → ( ∅ ·o 𝑥 ) = ( ∅ ·o ∅ ) )
2	1	eqeq1d	⊢ ( 𝑥 = ∅ → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o ∅ ) = ∅ ) )
3		oveq2	⊢ ( 𝑥 = 𝑦 → ( ∅ ·o 𝑥 ) = ( ∅ ·o 𝑦 ) )
4	3	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o 𝑦 ) = ∅ ) )
5		oveq2	⊢ ( 𝑥 = suc 𝑦 → ( ∅ ·o 𝑥 ) = ( ∅ ·o suc 𝑦 ) )
6	5	eqeq1d	⊢ ( 𝑥 = suc 𝑦 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o suc 𝑦 ) = ∅ ) )
7		oveq2	⊢ ( 𝑥 = 𝐴 → ( ∅ ·o 𝑥 ) = ( ∅ ·o 𝐴 ) )
8	7	eqeq1d	⊢ ( 𝑥 = 𝐴 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o 𝐴 ) = ∅ ) )
9		0elon	⊢ ∅ ∈ On
10		om0	⊢ ( ∅ ∈ On → ( ∅ ·o ∅ ) = ∅ )
11	9 10	ax-mp	⊢ ( ∅ ·o ∅ ) = ∅
12		oveq1	⊢ ( ( ∅ ·o 𝑦 ) = ∅ → ( ( ∅ ·o 𝑦 ) +o ∅ ) = ( ∅ +o ∅ ) )
13		omsuc	⊢ ( ( ∅ ∈ On ∧ 𝑦 ∈ On ) → ( ∅ ·o suc 𝑦 ) = ( ( ∅ ·o 𝑦 ) +o ∅ ) )
14	9 13	mpan	⊢ ( 𝑦 ∈ On → ( ∅ ·o suc 𝑦 ) = ( ( ∅ ·o 𝑦 ) +o ∅ ) )
15		oa0	⊢ ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
16	9 15	ax-mp	⊢ ( ∅ +o ∅ ) = ∅
17	16	eqcomi	⊢ ∅ = ( ∅ +o ∅ )
18	17	a1i	⊢ ( 𝑦 ∈ On → ∅ = ( ∅ +o ∅ ) )
19	14 18	eqeq12d	⊢ ( 𝑦 ∈ On → ( ( ∅ ·o suc 𝑦 ) = ∅ ↔ ( ( ∅ ·o 𝑦 ) +o ∅ ) = ( ∅ +o ∅ ) ) )
20	12 19	imbitrrid	⊢ ( 𝑦 ∈ On → ( ( ∅ ·o 𝑦 ) = ∅ → ( ∅ ·o suc 𝑦 ) = ∅ ) )
21		iuneq2	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∅ → ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∪ 𝑦 ∈ 𝑥 ∅ )
22		iun0	⊢ ∪ 𝑦 ∈ 𝑥 ∅ = ∅
23	21 22	eqtrdi	⊢ ( ∀ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∅ → ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∅ )
24		vex	⊢ 𝑥 ∈ V
25		omlim	⊢ ( ( ∅ ∈ On ∧ ( 𝑥 ∈ V ∧ Lim 𝑥 ) ) → ( ∅ ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) )
26	9 25	mpan	⊢ ( ( 𝑥 ∈ V ∧ Lim 𝑥 ) → ( ∅ ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) )
27	24 26	mpan	⊢ ( Lim 𝑥 → ( ∅ ·o 𝑥 ) = ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) )
28	27	eqeq1d	⊢ ( Lim 𝑥 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ∪ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∅ ) )
29	23 28	imbitrrid	⊢ ( Lim 𝑥 → ( ∀ 𝑦 ∈ 𝑥 ( ∅ ·o 𝑦 ) = ∅ → ( ∅ ·o 𝑥 ) = ∅ ) )
30	2 4 6 8 11 20 29	tfinds	⊢ ( 𝐴 ∈ On → ( ∅ ·o 𝐴 ) = ∅ )