Metamath Proof Explorer

Theorem omge1

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

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

Proof

Step	Hyp	Ref	Expression
1		3simpa	$⊢ (A \in On \land B \in On \land B \neq \emptyset) \to (A \in On \land B \in On)$
2		on0eln0	$⊢ B \in On \to (\emptyset \in B \leftrightarrow B \neq \emptyset)$
3	2	biimpar	$⊢ (B \in On \land B \neq \emptyset) \to \emptyset \in B$
4	3	3adant1	$⊢ (A \in On \land B \in On \land B \neq \emptyset) \to \emptyset \in B$
5		omword1	$⊢ ((A \in On \land B \in On) \land \emptyset \in B) \to A \subseteq A \cdot_{𝑜} B$
6	1 4 5	syl2anc	$⊢ (A \in On \land B \in On \land B \neq \emptyset) \to A \subseteq A \cdot_{𝑜} B$