Metamath Proof Explorer


Theorem om0

Description: Ordinal multiplication with zero. Definition 8.15(a) of TakeutiZaring p. 62. 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 ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )

Proof

Step Hyp Ref Expression
1 0elon ∅ ∈ On
2 omv ( ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ·o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) )
3 1 2 mpan2 ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) )
4 0ex ∅ ∈ V
5 4 rdg0 ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +o 𝐴 ) ) , ∅ ) ‘ ∅ ) = ∅
6 3 5 eqtrdi ( 𝐴 ∈ On → ( 𝐴 ·o ∅ ) = ∅ )