onmcl

Description: If an ordinal is less than a power of omega, the product with a natural number is also less than that power of omega. (Contributed by RP, 19-Feb-2025)

		Ref	Expression
	Assertion	onmcl	$⊢ (A \in On \land B \in On \land N \in ω) \to (A \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ A = \emptyset \to A \cdot_{𝑜} N = \emptyset \cdot_{𝑜} N$
2		simp3	$⊢ (A \in On \land B \in On \land N \in ω) \to N \in ω$
3		nnon	$⊢ N \in ω \to N \in On$
4		om0r	$⊢ N \in On \to \emptyset \cdot_{𝑜} N = \emptyset$
5	2 3 4	3syl	$⊢ (A \in On \land B \in On \land N \in ω) \to \emptyset \cdot_{𝑜} N = \emptyset$
6	1 5	sylan9eqr	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to A \cdot_{𝑜} N = \emptyset$
7		simpl2	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to B \in On$
8		omelon	$⊢ ω \in On$
9	7 8	jctil	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to (ω \in On \land B \in On)$
10		peano1	$⊢ \emptyset \in ω$
11		oen0	$⊢ ((ω \in On \land B \in On) \land \emptyset \in ω) \to \emptyset \in (ω ↑_{𝑜} B)$
12	9 10 11	sylancl	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to \emptyset \in (ω ↑_{𝑜} B)$
13	6 12	eqeltrd	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B)$
14	13	a1d	$⊢ ((A \in On \land B \in On \land N \in ω) \land A = \emptyset) \to (A \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$
15	2	adantr	$⊢ ((A \in On \land B \in On \land N \in ω) \land \emptyset \in A) \to N \in ω$
16		simp1	$⊢ (A \in On \land B \in On \land N \in ω) \to A \in On$
17	16	anim1i	$⊢ ((A \in On \land B \in On \land N \in ω) \land \emptyset \in A) \to (A \in On \land \emptyset \in A)$
18		ondif1	$⊢ A \in (On ∖ 1_{𝑜}) \leftrightarrow (A \in On \land \emptyset \in A)$
19	17 18	sylibr	$⊢ ((A \in On \land B \in On \land N \in ω) \land \emptyset \in A) \to A \in (On ∖ 1_{𝑜})$
20		simpl2	$⊢ ((A \in On \land B \in On \land N \in ω) \land \emptyset \in A) \to B \in On$
21		oveq2	$⊢ x = \emptyset \to A \cdot_{𝑜} x = A \cdot_{𝑜} \emptyset$
22	21	eleq1d	$⊢ x = \emptyset \to (A \cdot_{𝑜} x \in (ω ↑_{𝑜} B) \leftrightarrow A \cdot_{𝑜} \emptyset \in (ω ↑_{𝑜} B))$
23	22	imbi2d	$⊢ x = \emptyset \to ((((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} x \in (ω ↑_{𝑜} B)) \leftrightarrow (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} \emptyset \in (ω ↑_{𝑜} B)))$
24		oveq2	$⊢ x = y \to A \cdot_{𝑜} x = A \cdot_{𝑜} y$
25	24	eleq1d	$⊢ x = y \to (A \cdot_{𝑜} x \in (ω ↑_{𝑜} B) \leftrightarrow A \cdot_{𝑜} y \in (ω ↑_{𝑜} B))$
26	25	imbi2d	$⊢ x = y \to ((((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} x \in (ω ↑_{𝑜} B)) \leftrightarrow (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)))$
27		oveq2	$⊢ x = suc y \to A \cdot_{𝑜} x = A \cdot_{𝑜} suc y$
28	27	eleq1d	$⊢ x = suc y \to (A \cdot_{𝑜} x \in (ω ↑_{𝑜} B) \leftrightarrow A \cdot_{𝑜} suc y \in (ω ↑_{𝑜} B))$
29	28	imbi2d	$⊢ x = suc y \to ((((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} x \in (ω ↑_{𝑜} B)) \leftrightarrow (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} suc y \in (ω ↑_{𝑜} B)))$
30		oveq2	$⊢ x = N \to A \cdot_{𝑜} x = A \cdot_{𝑜} N$
31	30	eleq1d	$⊢ x = N \to (A \cdot_{𝑜} x \in (ω ↑_{𝑜} B) \leftrightarrow A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$
32	31	imbi2d	$⊢ x = N \to ((((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} x \in (ω ↑_{𝑜} B)) \leftrightarrow (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B)))$
33		eldifi	$⊢ A \in (On ∖ 1_{𝑜}) \to A \in On$
34		om0	$⊢ A \in On \to A \cdot_{𝑜} \emptyset = \emptyset$
35	33 34	syl	$⊢ A \in (On ∖ 1_{𝑜}) \to A \cdot_{𝑜} \emptyset = \emptyset$
36	35	adantr	$⊢ (A \in (On ∖ 1_{𝑜}) \land B \in On) \to A \cdot_{𝑜} \emptyset = \emptyset$
37	8	jctl	$⊢ B \in On \to (ω \in On \land B \in On)$
38	37 10 11	sylancl	$⊢ B \in On \to \emptyset \in (ω ↑_{𝑜} B)$
39	38	adantl	$⊢ (A \in (On ∖ 1_{𝑜}) \land B \in On) \to \emptyset \in (ω ↑_{𝑜} B)$
40	36 39	eqeltrd	$⊢ (A \in (On ∖ 1_{𝑜}) \land B \in On) \to A \cdot_{𝑜} \emptyset \in (ω ↑_{𝑜} B)$
41	40	adantr	$⊢ ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} \emptyset \in (ω ↑_{𝑜} B)$
42	33	adantr	$⊢ (A \in (On ∖ 1_{𝑜}) \land B \in On) \to A \in On$
43	42	ad2antrl	$⊢ (y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \to A \in On$
44		simpll	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to y \in ω$
45		onmsuc	$⊢ (A \in On \land y \in ω) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
46	43 44 45	syl2an2r	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} suc y = (A \cdot_{𝑜} y) +_{𝑜} A$
47		simpr	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)$
48		simplrr	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to A \in (ω ↑_{𝑜} B)$
49		eqid	$⊢ ω ↑_{𝑜} B = ω ↑_{𝑜} B$
50	49	jctl	$⊢ B \in On \to (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On)$
51	50	olcd	$⊢ B \in On \to (ω ↑_{𝑜} B = \emptyset \lor (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On))$
52	51	adantl	$⊢ (A \in (On ∖ 1_{𝑜}) \land B \in On) \to (ω ↑_{𝑜} B = \emptyset \lor (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On))$
53	52	ad2antrl	$⊢ (y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \to (ω ↑_{𝑜} B = \emptyset \lor (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On))$
54	53	adantr	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to (ω ↑_{𝑜} B = \emptyset \lor (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On))$
55		oacl2g	$⊢ ((A \cdot_{𝑜} y \in (ω ↑_{𝑜} B) \land A \in (ω ↑_{𝑜} B)) \land (ω ↑_{𝑜} B = \emptyset \lor (ω ↑_{𝑜} B = ω ↑_{𝑜} B \land B \in On))) \to (A \cdot_{𝑜} y) +_{𝑜} A \in (ω ↑_{𝑜} B)$
56	47 48 54 55	syl21anc	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to (A \cdot_{𝑜} y) +_{𝑜} A \in (ω ↑_{𝑜} B)$
57	46 56	eqeltrd	$⊢ ((y \in ω \land ((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B))) \land A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} suc y \in (ω ↑_{𝑜} B)$
58	57	exp31	$⊢ y \in ω \to (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to (A \cdot_{𝑜} y \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} suc y \in (ω ↑_{𝑜} B)))$
59	58	a2d	$⊢ y \in ω \to ((((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} y \in (ω ↑_{𝑜} B)) \to (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} suc y \in (ω ↑_{𝑜} B)))$
60	23 26 29 32 41 59	finds	$⊢ N \in ω \to (((A \in (On ∖ 1_{𝑜}) \land B \in On) \land A \in (ω ↑_{𝑜} B)) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$
61	60	expdimp	$⊢ (N \in ω \land (A \in (On ∖ 1_{𝑜}) \land B \in On)) \to (A \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$
62	15 19 20 61	syl12anc	$⊢ ((A \in On \land B \in On \land N \in ω) \land \emptyset \in A) \to (A \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$
63		on0eqel	$⊢ A \in On \to (A = \emptyset \lor \emptyset \in A)$
64	16 63	syl	$⊢ (A \in On \land B \in On \land N \in ω) \to (A = \emptyset \lor \emptyset \in A)$
65	14 62 64	mpjaodan	$⊢ (A \in On \land B \in On \land N \in ω) \to (A \in (ω ↑_{𝑜} B) \to A \cdot_{𝑜} N \in (ω ↑_{𝑜} B))$

Metamath Proof Explorer

Theorem onmcl

Proof