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 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 𝑜 =