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 ⊢ A ∈ On → ∅ ⋅ 𝑜 A = ∅

Proof

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