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{\cdot }_{𝑜}\varnothing =\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		om0	$$⊢A\in \mathrm{On}\to A{\cdot }_{𝑜}\varnothing =\varnothing$$
2	1	adantr	$$⊢\left(A\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to A{\cdot }_{𝑜}\varnothing =\varnothing$$
3		fnom	$$⊢{\cdot }_{𝑜}Fn\left(\mathrm{On}\times \mathrm{On}\right)$$
4		fndm	$$⊢{\cdot }_{𝑜}Fn\left(\mathrm{On}\times \mathrm{On}\right)\to \mathrm{dom}{\cdot }_{𝑜}=\mathrm{On}\times \mathrm{On}$$
5	3 4	ax-mp	$$⊢\mathrm{dom}{\cdot }_{𝑜}=\mathrm{On}\times \mathrm{On}$$
6	5	ndmov	$$⊢\neg \left(A\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to A{\cdot }_{𝑜}\varnothing =\varnothing$$
7	2 6	pm2.61i	$$⊢A{\cdot }_{𝑜}\varnothing =\varnothing$$