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 ( ๐ด ยทo โˆ… ) = โˆ…

Proof

Step Hyp Ref Expression
1 om0 โŠข ( ๐ด โˆˆ On โ†’ ( ๐ด ยทo โˆ… ) = โˆ… )
2 1 adantr โŠข ( ( ๐ด โˆˆ On โˆง โˆ… โˆˆ On ) โ†’ ( ๐ด ยทo โˆ… ) = โˆ… )
3 fnom โŠข ยทo Fn ( On ร— On )
4 3 fndmi โŠข dom ยทo = ( On ร— On )
5 4 ndmov โŠข ( ยฌ ( ๐ด โˆˆ On โˆง โˆ… โˆˆ On ) โ†’ ( ๐ด ยทo โˆ… ) = โˆ… )
6 2 5 pm2.61i โŠข ( ๐ด ยทo โˆ… ) = โˆ