Metamath Proof Explorer

Theorem oaordi3

Description: Ordinal addition of the same number on the left preserves the ordering of the numbers on the right. Lemma 3.6 of Schloeder p. 8. (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (A \in On \land B \in On \land C \in On) \to C \in On$
2		simp1	$⊢ (A \in On \land B \in On \land C \in On) \to A \in On$
3	1 2	jca	$⊢ (A \in On \land B \in On \land C \in On) \to (C \in On \land A \in On)$
4		oaordi	$⊢ (C \in On \land A \in On) \to (B \in C \to A +_{𝑜} B \in (A +_{𝑜} C))$
5	3 4	syl	$⊢ (A \in On \land B \in On \land C \in On) \to (B \in C \to A +_{𝑜} B \in (A +_{𝑜} C))$