om00el

Description: The product of two nonzero ordinal numbers is nonzero. (Contributed by NM, 28-Dec-2004)

		Ref	Expression
	Assertion	om00el	$⊢ (A \in On \land B \in On) \to (\emptyset \in (A \cdot_{𝑜} B) \leftrightarrow (\emptyset \in A \land \emptyset \in B))$

Step	Hyp	Ref	Expression
1		om00	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \lor B = \emptyset))$
2	1	necon3abid	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B \neq \emptyset \leftrightarrow \neg (A = \emptyset \lor B = \emptyset))$
3		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
4		on0eln0	$⊢ A \cdot_{𝑜} B \in On \to (\emptyset \in (A \cdot_{𝑜} B) \leftrightarrow A \cdot_{𝑜} B \neq \emptyset)$
5	3 4	syl	$⊢ (A \in On \land B \in On) \to (\emptyset \in (A \cdot_{𝑜} B) \leftrightarrow A \cdot_{𝑜} B \neq \emptyset)$
6		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
7		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
8	6 7	bi2anan9	$⊢ (A \in On \land B \in On) \to ((\emptyset \in A \land \emptyset \in B) \leftrightarrow (A \neq \emptyset \land B \neq \emptyset))$
9		neanior	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow \neg (A = \emptyset \lor B = \emptyset)$
10	8 9	bitrdi	$⊢ (A \in On \land B \in On) \to ((\emptyset \in A \land \emptyset \in B) \leftrightarrow \neg (A = \emptyset \lor B = \emptyset))$
11	2 5 10	3bitr4d	$⊢ (A \in On \land B \in On) \to (\emptyset \in (A \cdot_{𝑜} B) \leftrightarrow (\emptyset \in A \land \emptyset \in B))$

Metamath Proof Explorer