This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 .o (/) ) = (/)

Proof

Step Hyp Ref Expression
1 om0 
 |-  ( A e. On -> ( A .o (/) ) = (/) )
2 1 adantr 
 |-  ( ( A e. On /\ (/) e. On ) -> ( A .o (/) ) = (/) )
3 fnom 
 |-  .o Fn ( On X. On )
4 3 fndmi 
 |-  dom .o = ( On X. On )
5 4 ndmov 
 |-  ( -. ( A e. On /\ (/) e. On ) -> ( A .o (/) ) = (/) )
6 2 5 pm2.61i 
 |-  ( A .o (/) ) = (/)