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 imbitrrid ⊢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 imbitrrid ⊢Lim⁡x→∀y∈x∅⋅𝑜y=∅→∅⋅𝑜x=∅
30 2 4 6 8 11 20 29 tfinds ⊢A∈On→∅⋅𝑜A=∅