Metamath Proof Explorer


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 syl5ibr ( 𝑦 ∈ 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 syl5ibr ( Lim 𝑥 → ( ∀ 𝑦𝑥 ( ∅ ·o 𝑦 ) = ∅ → ( ∅ ·o 𝑥 ) = ∅ ) )
30 2 4 6 8 11 20 29 tfinds ( 𝐴 ∈ On → ( ∅ ·o 𝐴 ) = ∅ )