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		fndm	⊢ ( ·o Fn ( On × On ) → dom ·o = ( On × On ) )
5	3 4	ax-mp	⊢ dom ·o = ( On × On )
6	5	ndmov	⊢ ( ¬ ( 𝐴 ∈ On ∧ ∅ ∈ On ) → ( 𝐴 ·o ∅ ) = ∅ )
7	2 6	pm2.61i	⊢ ( 𝐴 ·o ∅ ) = ∅