Metamath Proof Explorer

Theorem om0

Description: Ordinal multiplication with zero. Definition 8.15(a) of TakeutiZaring p. 62. Definition 2.5 of Schloeder p. 4. See om0x for a way to remove the antecedent A e. On . (Contributed by NM, 17-Sep-1995) (Revised by Mario Carneiro, 8-Sep-2013)

Ref Expression
Assertion om0 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 omv ⊢ A ∈ On ∧ ∅ ∈ On → A ⋅ 𝑜 ∅ = rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ ∅
3 1 2 mpan2 ⊢ A ∈ On → A ⋅ 𝑜 ∅ = rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ ∅
4 0ex ⊢ ∅ ∈ V
5 4 rdg0 ⊢ rec ⁡ x ∈ V ⟼ x + 𝑜 A ∅ ⁡ ∅ = ∅
6 3 5 eqtrdi ⊢ A ∈ On → A ⋅ 𝑜 ∅ = ∅