omlimcl2

Description: The product of a limit ordinal with any nonzero ordinal is a limit ordinal. (Contributed by RP, 8-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		eloni	$⊢ A \in On \to Ord A$
2	1	ad2antrr	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to Ord A$
3		ne0i	$⊢ \emptyset \in A \to A \neq \emptyset$
4	3	adantl	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to A \neq \emptyset$
5		id	$⊢ A = ⋃ A \to A = ⋃ A$
6		df-lim	$⊢ Lim A \leftrightarrow (Ord A \land A \neq \emptyset \land A = ⋃ A)$
7	6	biimpri	$⊢ (Ord A \land A \neq \emptyset \land A = ⋃ A) \to Lim A$
8	2 4 5 7	syl2an3an	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = ⋃ A) \to Lim A$
9	8	ex	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (A = ⋃ A \to Lim A)$
10		limelon	$⊢ (B \in C \land Lim B) \to B \in On$
11	10	ad3antlr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land Lim A) \to B \in On$
12		simpll	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to A \in On$
13	12	anim1i	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land Lim A) \to (A \in On \land Lim A)$
14		0ellim	$⊢ Lim B \to \emptyset \in B$
15	14	adantl	$⊢ (B \in C \land Lim B) \to \emptyset \in B$
16	15	ad3antlr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land Lim A) \to \emptyset \in B$
17		omlimcl	$⊢ ((B \in On \land (A \in On \land Lim A)) \land \emptyset \in B) \to Lim (B \cdot_{𝑜} A)$
18	11 13 16 17	syl21anc	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land Lim A) \to Lim (B \cdot_{𝑜} A)$
19	18	ex	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (Lim A \to Lim (B \cdot_{𝑜} A))$
20	9 19	syld	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (A = ⋃ A \to Lim (B \cdot_{𝑜} A))$
21		onuni	$⊢ A \in On \to ⋃ A \in On$
22	21 10	anim12ci	$⊢ (A \in On \land (B \in C \land Lim B)) \to (B \in On \land ⋃ A \in On)$
23		omcl	$⊢ (B \in On \land ⋃ A \in On) \to B \cdot_{𝑜} ⋃ A \in On$
24	22 23	syl	$⊢ (A \in On \land (B \in C \land Lim B)) \to B \cdot_{𝑜} ⋃ A \in On$
25		simpr	$⊢ (A \in On \land (B \in C \land Lim B)) \to (B \in C \land Lim B)$
26	24 25	jca	$⊢ (A \in On \land (B \in C \land Lim B)) \to (B \cdot_{𝑜} ⋃ A \in On \land (B \in C \land Lim B))$
27	26	ad2antrr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to (B \cdot_{𝑜} ⋃ A \in On \land (B \in C \land Lim B))$
28		oalimcl	$⊢ (B \cdot_{𝑜} ⋃ A \in On \land (B \in C \land Lim B)) \to Lim ((B \cdot_{𝑜} ⋃ A) +_{𝑜} B)$
29	27 28	syl	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to Lim ((B \cdot_{𝑜} ⋃ A) +_{𝑜} B)$
30		simpr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to A = suc ⋃ A$
31	30	oveq2d	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to B \cdot_{𝑜} A = B \cdot_{𝑜} suc ⋃ A$
32	22	ad2antrr	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to (B \in On \land ⋃ A \in On)$
33		omsuc	$⊢ (B \in On \land ⋃ A \in On) \to B \cdot_{𝑜} suc ⋃ A = (B \cdot_{𝑜} ⋃ A) +_{𝑜} B$
34	32 33	syl	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to B \cdot_{𝑜} suc ⋃ A = (B \cdot_{𝑜} ⋃ A) +_{𝑜} B$
35	31 34	eqtrd	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to B \cdot_{𝑜} A = (B \cdot_{𝑜} ⋃ A) +_{𝑜} B$
36		limeq	$⊢ B \cdot_{𝑜} A = (B \cdot_{𝑜} ⋃ A) +_{𝑜} B \to (Lim (B \cdot_{𝑜} A) \leftrightarrow Lim ((B \cdot_{𝑜} ⋃ A) +_{𝑜} B))$
37	35 36	syl	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to (Lim (B \cdot_{𝑜} A) \leftrightarrow Lim ((B \cdot_{𝑜} ⋃ A) +_{𝑜} B))$
38	29 37	mpbird	$⊢ (((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \land A = suc ⋃ A) \to Lim (B \cdot_{𝑜} A)$
39	38	ex	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (A = suc ⋃ A \to Lim (B \cdot_{𝑜} A))$
40		orduniorsuc	$⊢ Ord A \to (A = ⋃ A \lor A = suc ⋃ A)$
41	2 40	syl	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to (A = ⋃ A \lor A = suc ⋃ A)$
42	20 39 41	mpjaod	$⊢ ((A \in On \land (B \in C \land Lim B)) \land \emptyset \in A) \to Lim (B \cdot_{𝑜} A)$

Metamath Proof Explorer

Theorem omlimcl2

Proof