Metamath Proof Explorer


Theorem om0x

Description: Ordinal multiplication with zero. Definition 8.15 of TakeutiZaring p. 62. Unlike om0 , this version works whether or not A is an ordinal. However, since it is an artifact of our particular function value definition outside the domain, we will not use it in order to be conventional and present it only as a curiosity. (Contributed by NM, 1-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion om0x A 𝑜 =

Proof

Step Hyp Ref Expression
1 om0 A On A 𝑜 =
2 1 adantr A On On A 𝑜 =
3 fnom 𝑜 Fn On × On
4 3 fndmi dom 𝑜 = On × On
5 4 ndmov ¬ A On On A 𝑜 =
6 2 5 pm2.61i A 𝑜 =