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 \cdot_{𝑜} \emptyset = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
2	1	adantr	$⊢ (A \in On \land \emptyset \in On) \to A \cdot_{𝑜} \emptyset = \emptyset$
3		fnom	$⊢ \cdot_{𝑜} Fn (On \times On)$
4	3	fndmi	$⊢ dom \cdot_{𝑜} = On \times On$
5	4	ndmov	$⊢ \neg (A \in On \land \emptyset \in On) \to A \cdot_{𝑜} \emptyset = \emptyset$
6	2 5	pm2.61i	$⊢ A \cdot_{𝑜} \emptyset = \emptyset$