Metamath Proof Explorer

Theorem omge2

Description: Any non-zero ordinal product is greater-than-or-equal to the term on the right. Lemma 3.12 of Schloeder p. 9. See omword2 . (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		ancom	$⊢ (A \in On \land B \in On) \leftrightarrow (B \in On \land A \in On)$
2	1	anbi1i	$⊢ ((A \in On \land B \in On) \land A \neq \emptyset) \leftrightarrow ((B \in On \land A \in On) \land A \neq \emptyset)$
3		df-3an	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \leftrightarrow ((A \in On \land B \in On) \land A \neq \emptyset)$
4		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
5	4	adantl	$⊢ (B \in On \land A \in On) \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
6	5	pm5.32i	$⊢ ((B \in On \land A \in On) \land \emptyset \in A) \leftrightarrow ((B \in On \land A \in On) \land A \neq \emptyset)$
7	2 3 6	3bitr4i	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \leftrightarrow ((B \in On \land A \in On) \land \emptyset \in A)$
8		omword2	$⊢ ((B \in On \land A \in On) \land \emptyset \in A) \to B \subseteq A \cdot_{𝑜} B$
9	7 8	sylbi	$⊢ (A \in On \land B \in On \land A \neq \emptyset) \to B \subseteq A \cdot_{𝑜} B$