om00

Description: The product of two ordinal numbers is zero iff at least one of them is zero. Proposition 8.22 of TakeutiZaring p. 64. (Contributed by NM, 21-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		neanior	$⊢ (A \neq \emptyset \land B \neq \emptyset) \leftrightarrow \neg (A = \emptyset \lor B = \emptyset)$
2		eloni	$⊢ A \in On \to Ord A$
3		ordge1n0	$⊢ Ord A \to (1_{𝑜} \subseteq A \leftrightarrow A \neq \emptyset)$
4	2 3	syl	$⊢ A \in On \to (1_{𝑜} \subseteq A \leftrightarrow A \neq \emptyset)$
5	4	biimprd	$⊢ A \in On \to (A \neq \emptyset \to 1_{𝑜} \subseteq A)$
6	5	adantr	$⊢ (A \in On \land B \in On) \to (A \neq \emptyset \to 1_{𝑜} \subseteq A)$
7		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
8	7	adantl	$⊢ (A \in On \land B \in On) \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
9		omword1	$⊢ ((A \in On \land B \in On) \land \emptyset \in B) \to A \subseteq A \cdot_{𝑜} B$
10	9	ex	$⊢ (A \in On \land B \in On) \to (\emptyset \in B \to A \subseteq A \cdot_{𝑜} B)$
11	8 10	sylbird	$⊢ (A \in On \land B \in On) \to (B \neq \emptyset \to A \subseteq A \cdot_{𝑜} B)$
12	6 11	anim12d	$⊢ (A \in On \land B \in On) \to ((A \neq \emptyset \land B \neq \emptyset) \to (1_{𝑜} \subseteq A \land A \subseteq A \cdot_{𝑜} B))$
13		sstr	$⊢ (1_{𝑜} \subseteq A \land A \subseteq A \cdot_{𝑜} B) \to 1_{𝑜} \subseteq A \cdot_{𝑜} B$
14	12 13	syl6	$⊢ (A \in On \land B \in On) \to ((A \neq \emptyset \land B \neq \emptyset) \to 1_{𝑜} \subseteq A \cdot_{𝑜} B)$
15	1 14	biimtrrid	$⊢ (A \in On \land B \in On) \to (\neg (A = \emptyset \lor B = \emptyset) \to 1_{𝑜} \subseteq A \cdot_{𝑜} B)$
16		omcl	$⊢ (A \in On \land B \in On) \to A \cdot_{𝑜} B \in On$
17		eloni	$⊢ A \cdot_{𝑜} B \in On \to Ord (A \cdot_{𝑜} B)$
18		ordge1n0	$⊢ Ord (A \cdot_{𝑜} B) \to (1_{𝑜} \subseteq A \cdot_{𝑜} B \leftrightarrow A \cdot_{𝑜} B \neq \emptyset)$
19	16 17 18	3syl	$⊢ (A \in On \land B \in On) \to (1_{𝑜} \subseteq A \cdot_{𝑜} B \leftrightarrow A \cdot_{𝑜} B \neq \emptyset)$
20	15 19	sylibd	$⊢ (A \in On \land B \in On) \to (\neg (A = \emptyset \lor B = \emptyset) \to A \cdot_{𝑜} B \neq \emptyset)$
21	20	necon4bd	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B = \emptyset \to (A = \emptyset \lor B = \emptyset))$
22		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} B = \emptyset \cdot_{𝑜} B$
23		om0r	$⊢ B \in On \to \emptyset \cdot_{𝑜} B = \emptyset$
24	22 23	sylan9eqr	$⊢ (B \in On \land A = \emptyset) \to A \cdot_{𝑜} B = \emptyset$
25	24	ex	$⊢ B \in On \to (A = \emptyset \to A \cdot_{𝑜} B = \emptyset)$
26	25	adantl	$⊢ (A \in On \land B \in On) \to (A = \emptyset \to A \cdot_{𝑜} B = \emptyset)$
27		oveq2	$⊢ B = \emptyset \to A \cdot_{𝑜} B = A \cdot_{𝑜} \emptyset$
28		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
29	27 28	sylan9eqr	$⊢ (A \in On \land B = \emptyset) \to A \cdot_{𝑜} B = \emptyset$
30	29	ex	$⊢ A \in On \to (B = \emptyset \to A \cdot_{𝑜} B = \emptyset)$
31	30	adantr	$⊢ (A \in On \land B \in On) \to (B = \emptyset \to A \cdot_{𝑜} B = \emptyset)$
32	26 31	jaod	$⊢ (A \in On \land B \in On) \to ((A = \emptyset \lor B = \emptyset) \to A \cdot_{𝑜} B = \emptyset)$
33	21 32	impbid	$⊢ (A \in On \land B \in On) \to (A \cdot_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \lor B = \emptyset))$

Metamath Proof Explorer

Theorem om00

Proof