Metamath Proof Explorer

Theorem oaword1

Description: An ordinal is less than or equal to its sum with another. Part of Exercise 5 of TakeutiZaring p. 62. Lemma 3.2 of Schloeder p. 7. (For the other part see oaord1 .) (Contributed by NM, 6-Dec-2004)

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

Proof

Step	Hyp	Ref	Expression
1		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
2	1	adantr	$⊢ (A \in On \land B \in On) \to A +_{𝑜} \emptyset = A$
3		0ss	$⊢ \emptyset \subseteq B$
4		0elon	$⊢ \emptyset \in On$
5		oaword	$⊢ (\emptyset \in On \land B \in On \land A \in On) \to (\emptyset \subseteq B \leftrightarrow A +_{𝑜} \emptyset \subseteq A +_{𝑜} B)$
6	5	3com13	$⊢ (A \in On \land B \in On \land \emptyset \in On) \to (\emptyset \subseteq B \leftrightarrow A +_{𝑜} \emptyset \subseteq A +_{𝑜} B)$
7	4 6	mp3an3	$⊢ (A \in On \land B \in On) \to (\emptyset \subseteq B \leftrightarrow A +_{𝑜} \emptyset \subseteq A +_{𝑜} B)$
8	3 7	mpbii	$⊢ (A \in On \land B \in On) \to A +_{𝑜} \emptyset \subseteq A +_{𝑜} B$
9	2 8	eqsstrrd	$⊢ (A \in On \land B \in On) \to A \subseteq A +_{𝑜} B$