Metamath Proof Explorer

Theorem omord2i

Description: Ordinal multiplication of the same non-zero number on the left preserves the ordering of the numbers on the right. Lemma 3.15 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

		Ref	Expression
	Assertion	omord2i	$⊢ ((A \in On \land A \neq \emptyset) \land C \in On) \to (B \in C \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C))$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in On \land A \neq \emptyset) \to A \in On$
2	1	anim1ci	$⊢ ((A \in On \land A \neq \emptyset) \land C \in On) \to (C \in On \land A \in On)$
3		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
4	3	biimpar	$⊢ (A \in On \land A \neq \emptyset) \to \emptyset \in A$
5	4	adantr	$⊢ ((A \in On \land A \neq \emptyset) \land C \in On) \to \emptyset \in A$
6		omordi	$⊢ ((C \in On \land A \in On) \land \emptyset \in A) \to (B \in C \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C))$
7	2 5 6	syl2anc	$⊢ ((A \in On \land A \neq \emptyset) \land C \in On) \to (B \in C \to A \cdot_{𝑜} B \in (A \cdot_{𝑜} C))$