oa00

Description: An ordinal sum is zero iff both of its arguments are zero. Lemma 3.10 of Schloeder p. 8. (Contributed by NM, 6-Dec-2004)

		Ref	Expression
	Assertion	oa00	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \land B = \emptyset))$

Proof

Step	Hyp	Ref	Expression
1		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
2	1	adantr	$⊢ (A \in On \land B \in On) \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
3		oaword1	$⊢ (A \in On \land B \in On) \to A \subseteq A +_{𝑜} B$
4	3	sseld	$⊢ (A \in On \land B \in On) \to (\emptyset \in A \to \emptyset \in (A +_{𝑜} B))$
5	2 4	sylbird	$⊢ (A \in On \land B \in On) \to (A \neq \emptyset \to \emptyset \in (A +_{𝑜} B))$
6		ne0i	$⊢ \emptyset \in (A +_{𝑜} B) \to A +_{𝑜} B \neq \emptyset$
7	5 6	syl6	$⊢ (A \in On \land B \in On) \to (A \neq \emptyset \to A +_{𝑜} B \neq \emptyset)$
8	7	necon4d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \to A = \emptyset)$
9		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
10	9	adantl	$⊢ (A \in On \land B \in On) \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
11		0elon	$⊢ \emptyset \in On$
12		oaord	$⊢ (\emptyset \in On \land B \in On \land A \in On) \to (\emptyset \in B \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
13	11 12	mp3an1	$⊢ (B \in On \land A \in On) \to (\emptyset \in B \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
14	13	ancoms	$⊢ (A \in On \land B \in On) \to (\emptyset \in B \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
15	10 14	bitr3d	$⊢ (A \in On \land B \in On) \to (B \neq \emptyset \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
16		ne0i	$⊢ A +_{𝑜} \emptyset \in (A +_{𝑜} B) \to A +_{𝑜} B \neq \emptyset$
17	15 16	biimtrdi	$⊢ (A \in On \land B \in On) \to (B \neq \emptyset \to A +_{𝑜} B \neq \emptyset)$
18	17	necon4d	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \to B = \emptyset)$
19	8 18	jcad	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \to (A = \emptyset \land B = \emptyset))$
20		oveq12	$⊢ (A = \emptyset \land B = \emptyset) \to A +_{𝑜} B = \emptyset +_{𝑜} \emptyset$
21		oa0	$⊢ \emptyset \in On \to \emptyset +_{𝑜} \emptyset = \emptyset$
22	11 21	ax-mp	$⊢ \emptyset +_{𝑜} \emptyset = \emptyset$
23	20 22	eqtrdi	$⊢ (A = \emptyset \land B = \emptyset) \to A +_{𝑜} B = \emptyset$
24	19 23	impbid1	$⊢ (A \in On \land B \in On) \to (A +_{𝑜} B = \emptyset \leftrightarrow (A = \emptyset \land B = \emptyset))$

Metamath Proof Explorer

Theorem oa00

Proof