This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 𝐴 ) = ∅ )