Metamath Proof Explorer

Theorem oaword2

Description: An ordinal is less than or equal to its sum with another. Theorem 21 of Suppes p. 209. Lemma 3.3 of Schloeder p. 7. (Contributed by NM, 7-Dec-2004)

		Ref	Expression
	Assertion	oaword2	$⊢ (A \in On \land B \in On) \to A \subseteq B +_{𝑜} A$

Proof

Step	Hyp	Ref	Expression
1		0ss	$⊢ \emptyset \subseteq B$
2		0elon	$⊢ \emptyset \in On$
3		oawordri	$⊢ (\emptyset \in On \land B \in On \land A \in On) \to (\emptyset \subseteq B \to \emptyset +_{𝑜} A \subseteq B +_{𝑜} A)$
4	2 3	mp3an1	$⊢ (B \in On \land A \in On) \to (\emptyset \subseteq B \to \emptyset +_{𝑜} A \subseteq B +_{𝑜} A)$
5		oa0r	$⊢ A \in On \to \emptyset +_{𝑜} A = A$
6	5	adantl	$⊢ (B \in On \land A \in On) \to \emptyset +_{𝑜} A = A$
7	6	sseq1d	$⊢ (B \in On \land A \in On) \to (\emptyset +_{𝑜} A \subseteq B +_{𝑜} A \leftrightarrow A \subseteq B +_{𝑜} A)$
8	4 7	sylibd	$⊢ (B \in On \land A \in On) \to (\emptyset \subseteq B \to A \subseteq B +_{𝑜} A)$
9	1 8	mpi	$⊢ (B \in On \land A \in On) \to A \subseteq B +_{𝑜} A$
10	9	ancoms	$⊢ (A \in On \land B \in On) \to A \subseteq B +_{𝑜} A$