Metamath Proof Explorer

Theorem oaord1

Description: An ordinal is less than its sum with a nonzero ordinal. Theorem 18 of Suppes p. 209 and its converse. (Contributed by NM, 6-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		0elon	$⊢ \emptyset \in On$
2		oaord	$⊢ (\emptyset \in On \land B \in On \land A \in On) \to (\emptyset \in B \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
3	1 2	mp3an1	$⊢ (B \in On \land A \in On) \to (\emptyset \in B \leftrightarrow A +_{𝑜} \emptyset \in (A +_{𝑜} B))$
4		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
5	4	adantl	$⊢ (B \in On \land A \in On) \to A +_{𝑜} \emptyset = A$
6	5	eleq1d	$⊢ (B \in On \land A \in On) \to (A +_{𝑜} \emptyset \in (A +_{𝑜} B) \leftrightarrow A \in (A +_{𝑜} B))$
7	3 6	bitrd	$⊢ (B \in On \land A \in On) \to (\emptyset \in B \leftrightarrow A \in (A +_{𝑜} B))$
8	7	ancoms	$⊢ (A \in On \land B \in On) \to (\emptyset \in B \leftrightarrow A \in (A +_{𝑜} B))$