Metamath Proof Explorer

Theorem oaord3

Description: When the same ordinal is added on the left, ordering of the sums is equivalent to the ordering of the ordinals on the right. Theorem 3.7 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		oaord	$⊢ (B \in On \land C \in On \land A \in On) \to (B \in C \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} C))$
2	1	3comr	$⊢ (A \in On \land B \in On \land C \in On) \to (B \in C \leftrightarrow A +_{𝑜} B \in (A +_{𝑜} C))$