oaltom

Description: Multiplication eventually dominates addition. (Contributed by RP, 3-Jan-2025)

		Ref	Expression
	Assertion	oaltom	$⊢ (A \in On \land B \in On) \to ((1_{𝑜} \in A \land A \in B) \to B +_{𝑜} A \in (B \cdot_{𝑜} A))$

Proof

Step	Hyp	Ref	Expression
1		om2	$⊢ B \in On \to B +_{𝑜} B = B \cdot_{𝑜} 2_{𝑜}$
2	1	ad2antlr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B +_{𝑜} B = B \cdot_{𝑜} 2_{𝑜}$
3		2on	$⊢ 2_{𝑜} \in On$
4	3	a1i	$⊢ (A \in On \land B \in On) \to 2_{𝑜} \in On$
5		simpl	$⊢ (A \in On \land B \in On) \to A \in On$
6		simpr	$⊢ (A \in On \land B \in On) \to B \in On$
7	4 5 6	3jca	$⊢ (A \in On \land B \in On) \to (2_{𝑜} \in On \land A \in On \land B \in On)$
8	7	adantr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to (2_{𝑜} \in On \land A \in On \land B \in On)$
9		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
10	9	a1i	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 2_{𝑜} = suc 1_{𝑜}$
11		simprl	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 1_{𝑜} \in A$
12		eloni	$⊢ A \in On \to Ord A$
13	12	adantr	$⊢ (A \in On \land B \in On) \to Ord A$
14	13	adantr	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to Ord A$
15	11 14	jca	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to (1_{𝑜} \in A \land Ord A)$
16		ordelsuc	$⊢ (1_{𝑜} \in A \land Ord A) \to (1_{𝑜} \in A \leftrightarrow suc 1_{𝑜} \subseteq A)$
17	16	biimpd	$⊢ (1_{𝑜} \in A \land Ord A) \to (1_{𝑜} \in A \to suc 1_{𝑜} \subseteq A)$
18	15 11 17	sylc	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to suc 1_{𝑜} \subseteq A$
19	10 18	eqsstrd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to 2_{𝑜} \subseteq A$
20		omwordi	$⊢ (2_{𝑜} \in On \land A \in On \land B \in On) \to (2_{𝑜} \subseteq A \to B \cdot_{𝑜} 2_{𝑜} \subseteq B \cdot_{𝑜} A)$
21	8 19 20	sylc	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B \cdot_{𝑜} 2_{𝑜} \subseteq B \cdot_{𝑜} A$
22	2 21	eqsstrd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B +_{𝑜} B \subseteq B \cdot_{𝑜} A$
23	6 6	jca	$⊢ (A \in On \land B \in On) \to (B \in On \land B \in On)$
24		simpr	$⊢ (1_{𝑜} \in A \land A \in B) \to A \in B$
25		oaordi	$⊢ (B \in On \land B \in On) \to (A \in B \to B +_{𝑜} A \in (B +_{𝑜} B))$
26	25	imp	$⊢ ((B \in On \land B \in On) \land A \in B) \to B +_{𝑜} A \in (B +_{𝑜} B)$
27	23 24 26	syl2an	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B +_{𝑜} A \in (B +_{𝑜} B)$
28	22 27	sseldd	$⊢ ((A \in On \land B \in On) \land (1_{𝑜} \in A \land A \in B)) \to B +_{𝑜} A \in (B \cdot_{𝑜} A)$
29	28	ex	$⊢ (A \in On \land B \in On) \to ((1_{𝑜} \in A \land A \in B) \to B +_{𝑜} A \in (B \cdot_{𝑜} A))$

Metamath Proof Explorer

Theorem oaltom

Proof