Metamath Proof Explorer

Theorem omlim2

Description: The nonzero product with an limit ordinal on the right is a limit ordinal. Lemma 3.13 of Schloeder p. 9. (Contributed by RP, 29-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in On \land A \neq \emptyset) \land (Lim B \land B \in V)) \to A \in On$
2		simpr	$⊢ ((A \in On \land A \neq \emptyset) \land (Lim B \land B \in V)) \to (Lim B \land B \in V)$
3	2	ancomd	$⊢ ((A \in On \land A \neq \emptyset) \land (Lim B \land B \in V)) \to (B \in V \land Lim B)$
4		on0eln0	$⊢ A \in On \to (\emptyset \in A \leftrightarrow A \neq \emptyset)$
5	4	biimpar	$⊢ (A \in On \land A \neq \emptyset) \to \emptyset \in A$
6	5	adantr	$⊢ ((A \in On \land A \neq \emptyset) \land (Lim B \land B \in V)) \to \emptyset \in A$
7		omlimcl	$⊢ ((A \in On \land (B \in V \land Lim B)) \land \emptyset \in A) \to Lim (A \cdot_{𝑜} B)$
8	1 3 6 7	syl21anc	$⊢ ((A \in On \land A \neq \emptyset) \land (Lim B \land B \in V)) \to Lim (A \cdot_{𝑜} B)$